aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/edit.ml
blob: e22c17ad519231aaf20b11c801a6d9087bfc0a6c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util

type ('a,'b,'c) t = {
  mutable focus : 'a option;
  mutable last_focused_stk : 'a list;
  buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }

let empty () = { 
  focus = None;
  last_focused_stk = [];
  buf = Hashtbl.create 17 }

let focus e nd =
  if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
  begin match e.focus with
    | Some foc when foc <> nd ->
        e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
    | _ -> ()
  end;
  e.focus <- Some nd

let unfocus e =
  match e.focus with
    | None -> invalid_arg "Edit.unfocus"
    | Some foc ->
	begin
	  e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
	  e.focus <- None
	end
    
let last_focused e =
  match e.last_focused_stk with
    | [] -> None
    | f::_ -> Some f

let restore_last_focus e =
  match e.last_focused_stk with
    | [] -> ()
    | f::_ -> focus e f
			     
let focusedp e =
  match e.focus with
    | None -> false
    | _    -> true

let read e =
  match e.focus with
    | None -> None
    | Some d ->
	let (bs,c) = Hashtbl.find e.buf d in
	Some(d,Bstack.top bs,c)

let mutate e f =
  match e.focus with
    | None -> invalid_arg "Edit.mutate"
    | Some d ->
	let (bs,c) = Hashtbl.find e.buf d in
	Bstack.app_push bs (f c)

let rev_mutate e f =
  match e.focus with
    | None -> invalid_arg "Edit.rev_mutate"
    | Some d ->
	let (bs,c) = Hashtbl.find e.buf d in
	Bstack.app_repl bs (f c)

let undo e n =
  match e.focus with
    | None -> invalid_arg "Edit.undo"
    | Some d ->
	let (bs,_) = Hashtbl.find e.buf d in
	if Bstack.depth bs = 1 & n > 0 then
	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
        repeat n Bstack.pop bs

let create e (d,b,c,udepth) =
  if Hashtbl.mem e.buf d then
    errorlabstrm "Edit.create" 
      (str"Already editing something of that name");
  let bs = Bstack.create udepth b in
  Hashtbl.add e.buf d (bs,c)

let delete e d =
  if not(Hashtbl.mem e.buf d) then
    errorlabstrm "Edit.delete" (str"No such editor");
  Hashtbl.remove e.buf d;
  e.last_focused_stk <- (list_except d e.last_focused_stk);
  match e.focus with
    | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
    | None -> ()

let dom e = 
  let l = ref [] in
  Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
  !l
	      
let clear e =
  e.focus <- None;
  e.last_focused_stk <- [];
  Hashtbl.clear e.buf