← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/edit.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/edit.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: edit.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
 
 
14
type ('a,'b,'c) t = {
 
15
  mutable focus : 'a option;
 
16
  mutable last_focused_stk : 'a list;
 
17
  buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
 
18
 
 
19
let empty () = { 
 
20
  focus = None;
 
21
  last_focused_stk = [];
 
22
  buf = Hashtbl.create 17 }
 
23
 
 
24
let focus e nd =
 
25
  if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
 
26
  begin match e.focus with
 
27
    | Some foc when foc <> nd ->
 
28
        e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
 
29
    | _ -> ()
 
30
  end;
 
31
  e.focus <- Some nd
 
32
 
 
33
let unfocus e =
 
34
  match e.focus with
 
35
    | None -> invalid_arg "Edit.unfocus"
 
36
    | Some foc ->
 
37
        begin
 
38
          e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
 
39
          e.focus <- None
 
40
        end
 
41
    
 
42
let last_focused e =
 
43
  match e.last_focused_stk with
 
44
    | [] -> None
 
45
    | f::_ -> Some f
 
46
 
 
47
let restore_last_focus e =
 
48
  match e.last_focused_stk with
 
49
    | [] -> ()
 
50
    | f::_ -> focus e f
 
51
                             
 
52
let focusedp e =
 
53
  match e.focus with
 
54
    | None -> false
 
55
    | _    -> true
 
56
 
 
57
let read e =
 
58
  match e.focus with
 
59
    | None -> None
 
60
    | Some d ->
 
61
        let (bs,c) = Hashtbl.find e.buf d in
 
62
        Some(d,Bstack.top bs,c)
 
63
 
 
64
let mutate e f =
 
65
  match e.focus with
 
66
    | None -> invalid_arg "Edit.mutate"
 
67
    | Some d ->
 
68
        let (bs,c) = Hashtbl.find e.buf d in
 
69
        Bstack.app_push bs (f c)
 
70
 
 
71
let rev_mutate e f =
 
72
  match e.focus with
 
73
    | None -> invalid_arg "Edit.rev_mutate"
 
74
    | Some d ->
 
75
        let (bs,c) = Hashtbl.find e.buf d in
 
76
        Bstack.app_repl bs (f c)
 
77
 
 
78
let undo e n =
 
79
  match e.focus with
 
80
    | None -> invalid_arg "Edit.undo"
 
81
    | Some d ->
 
82
        let (bs,_) = Hashtbl.find e.buf d in
 
83
        if n >= Bstack.size bs then
 
84
          errorlabstrm "Edit.undo" (str"Undo stack exhausted");
 
85
        repeat n Bstack.pop bs
 
86
 
 
87
(* Return the depth of the focused proof of [e] stack, this is used to
 
88
   put informations in coq prompt (in emacs mode). *)
 
89
let depth e =
 
90
  match e.focus with
 
91
    | None -> invalid_arg "Edit.depth"
 
92
    | Some d ->
 
93
        let (bs,_) = Hashtbl.find e.buf d in
 
94
        Bstack.depth bs
 
95
 
 
96
(* Undo focused proof of [e] to reach depth [n] *)
 
97
let undo_todepth e n =
 
98
  match e.focus with
 
99
    | None -> 
 
100
        if n <> 0 
 
101
        then errorlabstrm "Edit.undo_todepth" (str"No proof in progress")
 
102
        else () (* if there is no proof in progress, then n must be zero *)
 
103
    | Some d ->
 
104
        let (bs,_) = Hashtbl.find e.buf d in
 
105
        let ucnt = Bstack.depth bs - n in
 
106
        if  ucnt >= Bstack.size bs then
 
107
          errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
 
108
        repeat ucnt Bstack.pop bs
 
109
 
 
110
let create e (d,b,c,usize) =
 
111
  if Hashtbl.mem e.buf d then
 
112
    errorlabstrm "Edit.create" 
 
113
      (str"Already editing something of that name");
 
114
  let bs = Bstack.create usize b in
 
115
  Hashtbl.add e.buf d (bs,c)
 
116
 
 
117
let delete e d =
 
118
  if not(Hashtbl.mem e.buf d) then
 
119
    errorlabstrm "Edit.delete" (str"No such editor");
 
120
  Hashtbl.remove e.buf d;
 
121
  e.last_focused_stk <- (list_except d e.last_focused_stk);
 
122
  match e.focus with
 
123
    | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
 
124
    | None -> ()
 
125
 
 
126
let dom e = 
 
127
  let l = ref [] in
 
128
  Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
 
129
  !l
 
130
              
 
131
let clear e =
 
132
  e.focus <- None;
 
133
  e.last_focused_stk <- [];
 
134
  Hashtbl.clear e.buf