diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:52 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-10 11:22:52 +0000 |
commit | e0f8d741b933361fc33a4ccd683b0137c869c468 (patch) | |
tree | 04a0eb2cf4a90bca2bf9c9220cdb87bbedfabeff | |
parent | 81cddc53da47e26bb43771e46e9a1ce03de60d60 (diff) |
CoqIDE: move cmd_stack to a separate module: Document
The idea is to move the logic related to document handling
to a separate module that can be tested by fake_ide too.
CoqOps should "only" interface Document with the GtkTextBuffer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.build | 8 | ||||
-rw-r--r-- | ide/coqOps.ml | 206 | ||||
-rw-r--r-- | ide/document.ml | 211 | ||||
-rw-r--r-- | ide/document.mli | 126 |
4 files changed, 315 insertions, 236 deletions
diff --git a/Makefile.build b/Makefile.build index 99ef062b9..964a4694f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -541,9 +541,13 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) tools/fake_ide$(BESTOBJ) +tools/fake_ide.cmo: COND_BYTEFLAGS+=-I ide + +tools/fake_ide.cmx: COND_OPTFLAGS+=-I ide + +$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) ide/document$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix) + $(HIDE)$(call bestocaml,-I ide,str unix) # votour: a small vo explorer (based on the checker) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index e9f29fba1..1246d3159 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -30,13 +30,11 @@ module SentenceId : sig mutable flags : flag list; mutable tooltips : (int * int * string lazy_t) list; edit_id : int; - mutable state_id : Stateid.t option; } val mk_sentence : start:GText.mark -> stop:GText.mark -> flag list -> sentence - val assign_state_id : sentence -> Stateid.t -> unit val set_flags : sentence -> flag list -> unit val add_flag : sentence -> flag -> unit val has_flag : sentence -> mem_flag -> bool @@ -46,7 +44,8 @@ module SentenceId : sig val find_all_tooltips : sentence -> int -> string lazy_t list val add_tooltip : sentence -> int -> int -> string lazy_t -> unit - val dbg_to_string : GText.buffer -> sentence -> string + val dbg_to_string : + GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds end = struct @@ -56,7 +55,6 @@ end = struct mutable flags : flag list; mutable tooltips : (int * int * string lazy_t) list; edit_id : int; - mutable state_id : Stateid.t option; } let id = ref 0 @@ -65,36 +63,32 @@ end = struct stop = stop; flags = flags; edit_id = !id; - state_id = None; tooltips = []; } let hidden_edit_id () = decr id; !id - let assign_state_id s id = - assert(s.state_id = None); - assert(id <> Stateid.dummy); - s.state_id <- Some id let set_flags s f = s.flags <- f let add_flag s f = s.flags <- CList.add_set f s.flags let has_flag s mf = List.exists (fun f -> mem_flag_of_flag f = mf) s.flags let remove_flag s mf = s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags - let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id + let same_sentence s1 s2 = s1.edit_id = s2.edit_id let find_all_tooltips s off = CList.map_filter (fun (start,stop,t) -> if start <= off && off <= stop then Some t else None) s.tooltips let add_tooltip s a b t = s.tooltips <- (a,b,t) :: s.tooltips - let dbg_to_string (b : GText.buffer) s = + let dbg_to_string (b : GText.buffer) focused id s = let ellipsize s = Str.global_replace (Str.regexp "^[\n ]*") "" (if String.length s > 20 then String.sub s 0 17 ^ "..." else s) in - Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s] %s" + Pp.str (Printf.sprintf "%s[%3d,%3s](%5d,%5d) %s [%s] %s" + (if focused then "*" else " ") s.edit_id - (Stateid.to_string (Option.default Stateid.dummy s.state_id)) + (Stateid.to_string (Option.default Stateid.dummy id)) (b#get_iter_at_mark s.start)#offset (b#get_iter_at_mark s.stop)#offset (ellipsize @@ -103,7 +97,7 @@ end = struct (ellipsize (String.concat "," (List.map (fun (a,b,t) -> - Printf.sprintf "<%d,%d> %s" a b (Lazy.force t)) s.tooltips))) + Printf.sprintf "<%d,%d> %s" a b (Lazy.force t)) s.tooltips)))) end @@ -137,6 +131,8 @@ object method destroy : unit -> unit end +module Doc = Document + class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) @@ -149,7 +145,7 @@ object(self) val proof = _pv val messages = _mv - val cmd_stack = Document.create () + val document : sentence Doc.document = Doc.create () val mutable initial_state = Stateid.initial @@ -175,16 +171,16 @@ object(self) let marks = iter#marks in if marks = [] then aux iter#backward_char else - let mem_marks s _ = + let mem_marks _ _ s = List.exists (fun m -> Gobject.get_oid m = Gobject.get_oid (buffer#get_mark s.start)) marks in - try Document.find mem_marks cmd_stack + try Doc.find document mem_marks with Not_found -> aux iter#backward_char in aux iter in let ss = - find_all_tooltips s - (iter#offset - (buffer#get_iter_at_mark s.start)#offset) in + find_all_tooltips s.Doc.data + (iter#offset - (buffer#get_iter_at_mark s.Doc.data.start)#offset) in let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON; script#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>") @@ -197,26 +193,19 @@ object(self) feedback_timer.Ideutils.kill () method private print_stack = - Minilib.log "cmd_stack:"; - let top, mid, bot = Document.to_lists cmd_stack in - Minilib.log "--start--"; - List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) top; - if Document.focused cmd_stack then Minilib.log "----"; - List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) mid; - if Document.focused cmd_stack then Minilib.log "----"; - List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) bot; - Minilib.log "--stop--" + Minilib.log "document:"; + Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer))) method private enter_focus start stop to_id tip = - if Document.focused cmd_stack then begin + if Doc.focused document then begin self#exit_focus tip end; - let at id s = s.state_id = Some id in + let at id s = s.Doc.state_id = Some id in self#print_stack; Minilib.log("Focusing "^Stateid.to_string start^" "^Stateid.to_string stop); - Document.focus cmd_stack ~cond_top:(at start) ~cond_bot:(at stop); + Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop); self#print_stack; - let qed_s = Document.tip cmd_stack in + let qed_s = Doc.tip_data document in buffer#apply_tag Tags.Script.read_only ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char (fun c -> not(Glib.Unichar.isspace c))) @@ -227,15 +216,15 @@ object(self) method private exit_focus newtip = self#print_stack; Minilib.log "Unfocusing"; - Document.unfocus cmd_stack; + Doc.unfocus document; self#print_stack; - if (Some newtip <> (Document.tip cmd_stack).state_id) then begin + if (Some newtip <> (Doc.tip document).Doc.state_id) then begin Minilib.log ("Cutting tip to " ^ Stateid.to_string newtip); - let until _ id _ _ = id = Some newtip in + let until id _ _ = id = Some newtip in let n, _, _, seg = self#segment_to_be_cleared until in self#cleanup n seg end; - let where = buffer#get_iter_at_mark (Document.tip cmd_stack).stop in + let where = buffer#get_iter_at_mark (Doc.tip_data document).stop in buffer#move_mark ~where (`NAME "start_of_input"); buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input") @@ -281,7 +270,8 @@ object(self) Coq.bind (Coq.seq action query) next method private mark_as_needed sentence = - Minilib.log("Marking " ^ dbg_to_string buffer sentence); + Minilib.log("Marking " ^ + Pp.string_of_ppcmds (dbg_to_string buffer false None sentence)); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in @@ -327,34 +317,34 @@ object(self) let msg = Queue.pop feedbacks in let id = msg.id in let sentence = - let finder s _ = - match s.state_id, id with - | Some id', State id when id = id' -> Some s - | _, Edit id when id = s.edit_id -> Some s + let finder _ state_id s = + match state_id, id with + | Some id', State id when Stateid.equal id id' -> Some (state_id, s) + | _, Edit id when id = s.edit_id -> Some (state_id, s) | _ -> None in - try Some (Document.find_map finder cmd_stack) + try Some (Doc.find_map document finder) with Not_found -> None in - let log s sentence = + let log s state_id = Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string - (Option.default Stateid.dummy sentence.state_id)) in + (Option.default Stateid.dummy state_id)) in begin match msg.content, sentence with - | AddedAxiom, Some sentence -> - log "AddedAxiom" sentence; + | AddedAxiom, Some (id,sentence) -> + log "AddedAxiom" id; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; add_flag sentence `UNSAFE; self#mark_as_needed sentence - | Processed, Some sentence -> - log "Processed" sentence; + | Processed, Some (id,sentence) -> + log "Processed" id; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; self#mark_as_needed sentence - | GlobRef(loc, filepath, modpath, ident, ty), Some sentence -> - log "GlobRef" sentence; + | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> + log "GlobRef" id; self#attach_tooltip sentence loc (Printf.sprintf "%s %s %s" filepath ident ty) - | ErrorMsg(loc, msg), Some sentence -> - log "ErrorMsg" sentence; + | ErrorMsg(loc, msg), Some (id,sentence) -> + log "ErrorMsg" id; remove_flag sentence `PROCESSING; add_flag sentence (`ERROR msg); self#mark_as_needed sentence; @@ -367,9 +357,9 @@ object(self) | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" - else if Document.is_empty cmd_stack then () + else if Doc.is_empty document then () else - match id, (Document.tip cmd_stack).state_id with + match id, (Doc.tip document).Doc.state_id with | Edit _, _ -> () | State id1, Some id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks (* Put back into the queue *) @@ -419,15 +409,15 @@ object(self) condition returns true; it is fed with the number of phrases read and the iters enclosing the current sentence. *) method private fill_command_queue until queue = - let rec loop len iter = + let rec loop iter = match Sentence.find buffer iter with | None -> () | Some (start, stop) -> - if until len start stop then begin + if until start stop then begin () end else if start#has_tag Tags.Script.processed then begin Queue.push (`Skip (start, stop)) queue; - loop len stop + loop stop end else begin buffer#apply_tag Tags.Script.to_process ~start ~stop; (* Check if this is a comment *) @@ -440,10 +430,10 @@ object(self) ~stop:(`MARK (buffer#create_mark stop)) (if is_comment then [`COMMENT] else []) in Queue.push (`Sentence sentence) queue; - if not stop#is_end then loop (succ len) stop + if not stop#is_end then loop stop end in - loop 0 self#get_start_of_input + loop self#get_start_of_input method private discard_command_queue queue = while not (Queue.is_empty queue) do @@ -474,9 +464,9 @@ object(self) queue) in let tip = - try Document.fold_until (fun () -> function - | { state_id = Some id } -> Stop id - | _ -> Next ()) () cmd_stack + try Doc.fold_until document () (fun () -> function + | Some id -> fun _ -> Stop id + | _ -> fun _ -> Next ()) with Not_found -> initial_state in Coq.bind action (fun queue -> let rec loop tip topstack = @@ -485,18 +475,19 @@ object(self) let () = script#recenter_insert in match topstack with | [] -> self#show_goals - | s :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) + | s :: _ -> + self#backtrack_to_iter (buffer#get_iter_at_mark s.Doc.data.start) else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> assert false | `Skip(start,stop), s :: topstack -> - assert(start#equal (buffer#get_iter_at_mark s.start)); - assert(stop#equal (buffer#get_iter_at_mark s.stop)); + assert(start#equal (buffer#get_iter_at_mark s.Doc.data.start)); + assert(stop#equal (buffer#get_iter_at_mark s.Doc.data.stop)); loop tip topstack | `Sentence sentence, _ :: _ -> assert false | `Sentence sentence, [] -> add_flag sentence `PROCESSING; - Document.push sentence cmd_stack; + Doc.push document sentence; if has_flag sentence `COMMENT then let () = remove_flag sentence `PROCESSING in let () = self#commit_queue_transaction sentence in @@ -508,21 +499,21 @@ object(self) Coq.add ~logger:push_msg ((phrase,sentence.edit_id),(tip,verbose))in let next = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> - assign_state_id sentence id; + Doc.assign_tip_id document id; push_msg Notice msg; self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> - assign_state_id sentence id; - let topstack, _, _ = Document.to_lists cmd_stack in + Doc.assign_tip_id document id; + let topstack, _, _ = Doc.to_lists document in self#exit_focus tip; push_msg Notice msg; self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) | Fail (id, loc, msg) -> - let sentence = Document.pop cmd_stack in - self#process_interp_error queue sentence loc msg id + let sentence = Doc.pop document in + self#process_interp_error queue sentence.Doc.data loc msg id in Coq.bind query next in @@ -532,7 +523,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Info "Document checked"; + messages#push Info "Doc checked"; Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -541,8 +532,8 @@ object(self) method get_n_errors = List.fold_left - (fun n s -> if has_flag s `ERROR then n+1 else n) - 0 (Document.to_list cmd_stack) + (fun n s -> if has_flag s.Doc.data `ERROR then n+1 else n) + 0 (Doc.to_list document) method get_errors = let extract_error s = @@ -550,19 +541,19 @@ object(self) | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg | _ -> assert false in CList.map_filter (fun s -> - if has_flag s `ERROR then Some (extract_error s) + if has_flag s.Doc.data `ERROR then Some (extract_error s.Doc.data) else None) - (Document.to_list cmd_stack) + (Doc.to_list document) method process_next_phrase = - let until len start stop = 1 <= len in + let until = let len = ref 0 in fun _ _ -> incr len; !len > 1 in let next () = buffer#place_cursor ~where:self#get_start_of_input; Coq.return () in Coq.bind (self#process_until until true) next method private process_until_iter iter = - let until len start stop = + let until start stop = if prefs.Preferences.stop_before then stop#compare iter > 0 else start#compare iter >= 0 in @@ -573,33 +564,33 @@ object(self) (* finds the state_id and if it an unfocus is needed to reach it *) method private find_id until = + let focused = Doc.focused document in try - Document.find_map - (function - | { start; stop; state_id = Some id } -> fun b -> - if until 0 (Some id) start stop then - Some (id, if Document.focused cmd_stack then not b else false) - else - None - | { start; stop; state_id = None } -> fun _ -> None) - cmd_stack - with Not_found -> initial_state, Document.focused cmd_stack + Doc.find_map document (fun b -> + function + | Some id -> fun { start; stop } -> + if until (Some id) start stop then + Some (id, if focused then not b else false) + else + None + | None -> fun { start; stop } -> None) + with Not_found -> initial_state, focused method private segment_to_be_cleared until = - let finder (n, found, zone) ({ start; stop; state_id } as sentence) = - let found = found || until n state_id start stop in + let finder (n, found, zone) state_id ({ start; stop } as sentence) = + let found = found || until state_id start stop in match found, state_id with | true, Some id -> Stop (n, id, Some sentence, zone) | _ -> Next (n + 1, found, sentence :: zone) in - try Document.fold_until finder (0, false, []) cmd_stack + try Doc.fold_until document (0, false, []) finder with Not_found -> - Minilib.log "ALL"; - Document.length cmd_stack, initial_state, - None, List.rev (Document.to_list cmd_stack) + Minilib.log "XXX ALL XXX"; + Doc.length document, initial_state, + None, List.rev (List.map (fun x -> x.Doc.data) (Doc.to_list document)) method private cleanup n seg = Minilib.log("Clean "^string_of_int n^" "^string_of_int(List.length seg)); - for i = 1 to n do ignore(Document.pop cmd_stack) done; + for i = 1 to n do ignore(Doc.pop document) done; if seg <> [] then begin let start = buffer#get_iter_at_mark (CList.hd seg).start in let stop = buffer#get_iter_at_mark (CList.last seg).stop in @@ -638,7 +629,7 @@ object(self) if unfocus_needed then self#exit_focus to_id else begin let n, to_id, sentence, seg = - self#segment_to_be_cleared (fun _ id _ _ -> id = Some to_id) in + self#segment_to_be_cleared (fun id _ _ -> id = Some to_id) in self#cleanup n seg end; conclusion () @@ -647,19 +638,19 @@ object(self) else begin self#enter_focus start_id stop_id to_id tip; let n, to_id, sentence, seg = - self#segment_to_be_cleared (fun _ id _ _ -> id = Some to_id) in + self#segment_to_be_cleared (fun id _ _ -> id = Some to_id) in self#cleanup n seg end; conclusion () | Fail (safe_id, loc, msg) -> if loc <> None then messages#push Error "Fixme LOC"; messages#push Error msg; - undo (fun _ id _ _ -> id = Some safe_id)) + undo (fun id _ _ -> id = Some safe_id)) in undo until) method private backtrack_to_iter ?move_insert iter = - let until _ _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in + let until _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in self#backtrack_until ?move_insert until method handle_failure (safe_id, (loc : (int * int) option), msg) = @@ -669,12 +660,13 @@ object(self) ignore(self#process_feedback ()); Coq.seq (self#backtrack_until ~move_insert:false - (fun _ id _ _ -> id = Some safe_id)) + (fun id _ _ -> id = Some safe_id)) (Coq.lift (fun () -> script#scroll_mark_onscreen (`NAME "start_of_input"))) method backtrack_last_phrase = - let until n _ _ _ = n >= 1 in + let id = (Doc.tip document).Doc.state_id in + let until sid _ _ = sid <> id in messages#clear; self#backtrack_until until @@ -710,7 +702,7 @@ object(self) ~start:(`MARK (buffer#create_mark start)) ~stop:(`MARK (buffer#create_mark stop)) [] in - Document.push sentence cmd_stack; + Doc.push document sentence; messages#clear; self#show_goals in @@ -744,11 +736,11 @@ object(self) let action () = if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."; (* clear the stack *) - if Document.focused cmd_stack then Document.unfocus cmd_stack; - while not (Document.is_empty cmd_stack) do - let phrase = Document.pop cmd_stack in - buffer#delete_mark phrase.start; - buffer#delete_mark phrase.stop + if Doc.focused document then Doc.unfocus document; + while not (Doc.is_empty document) do + let phrase = Doc.pop document in + buffer#delete_mark phrase.Doc.data.start; + buffer#delete_mark phrase.Doc.data.stop done; List.iter (buffer#remove_tag ~start:buffer#start_iter ~stop:buffer#end_iter) diff --git a/ide/document.ml b/ide/document.ml index 96ec05624..9b048320a 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -6,94 +6,153 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -exception Empty = Stack.Empty +exception Empty -type 'a t = { - mutable stack : 'a list; - mutable context : ('a list * 'a list) option -} +let invalid_arg s = raise (Invalid_argument ("Document."^s)) + +type 'a sentence = { mutable state_id : Stateid.t option; data : 'a } +type id = Stateid.t +type 'a document = { + mutable stack : 'a sentence list; + mutable context : ('a sentence list * 'a sentence list) option +} + let create () = { stack = []; context = None } -let push x s = s.stack <- x :: s.stack - -let pop = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::xs } as s -> s.stack <- xs; x +(* Invariant, only the tip is a allowed to have state_id = None *) +let invariant l = l = [] || (List.hd l).state_id <> None let tip = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::_ } -> x + | { stack = [] } -> raise Empty + | { stack = { state_id = Some id }::_ } -> id + | { stack = { state_id = None }::_ } -> invalid_arg "tip" + +let tip_data = function + | { stack = [] } -> raise Empty + | { stack = { data }::_ } -> data + +let push d x = + assert(invariant d.stack); + d.stack <- { data = x; state_id = None } :: d.stack -let to_list = function - | { context = None; stack = s } -> s - | { context = Some (a,b); stack = s } -> a @ s @ b +let pop = function + | { stack = [] } -> raise Empty + | { stack = { data }::xs } as s -> s.stack <- xs; data + +let focus d ~cond_top:c_start ~cond_bot:c_stop = + assert(invariant d.stack); + if d.context <> None then invalid_arg "focus"; + let rec aux (a,s,b) grab = function + | [] -> invalid_arg "focus" + | { state_id = Some id; data } as x :: xs when not grab -> + if c_start id data then aux (a,s,b) true (x::xs) + else aux (x::a,s,b) grab xs + | { state_id = Some id; data } as x :: xs -> + if c_stop id data then List.rev a, List.rev (x::s), xs + else aux (a,x::s,b) grab xs + | _ -> assert false in + let a, s, b = aux ([],[],[]) false d.stack in + d.stack <- s; + d.context <- Some (a, b) + +let unfocus = function + | { context = None } -> invalid_arg "unfocus" + | { context = Some (a,b); stack } as d -> + assert(invariant stack); + d.context <- None; + d.stack <- a @ stack @ b + +let focused { context } = context <> None let to_lists = function | { context = None; stack = s } -> [],s,[] | { context = Some (a,b); stack = s } -> a,s,b -let find f s = - let a, s, b = to_lists s in - try List.find (fun x -> f x false) a with Not_found -> - try List.find (fun x -> f x true) s with Not_found -> - List.find (fun x -> f x false) b - -let find_map f s = - let rec aux b = function - | [] -> raise Not_found - | x :: xs -> match f x b with None -> aux b xs | Some i -> i - in - let a, s, b = to_lists s in - try aux false a with Not_found -> - try aux true s with Not_found -> - aux false b - -type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c - -let fold_until f accu s = - let rec aux accu = function - | [] -> raise Not_found - | x :: xs -> match f accu x with Stop x -> x | Next i -> aux i xs in - aux accu s.stack - +let flat f b = fun x -> f b x.state_id x.data + +let find d f = + let a, s, b = to_lists d in + ( + try List.find (flat f false) a with Not_found -> + try List.find (flat f true) s with Not_found -> + List.find (flat f false) b + ).data + +let find_map d f = + let a, s, b = to_lists d in + try CList.find_map (flat f false) a with Not_found -> + try CList.find_map (flat f true) s with Not_found -> + CList.find_map (flat f false) b + let is_empty = function | { stack = []; context = None } -> true | _ -> false - -let iter f = function - | { stack = s; context = None } -> List.iter (fun x -> f x true) s - | { stack = s; context = Some(a,b) } -> - List.iter (fun x -> f x false) a; - List.iter (fun x -> f x true) s; - List.iter (fun x -> f x false) b - -let clear s = s.stack <- []; s.context <- None - -let length = function - | { stack = s; context = None } -> List.length s - | { stack = s; context = Some(a,b) } -> - List.length a + List.length s + List.length b - -let focus s ~cond_top:c_start ~cond_bot:c_stop = - if s.context <> None then raise (Invalid_argument "CStack.focus"); - let rec aux (a,s,b) grab = function - | [] -> raise (Invalid_argument "CStack.focus") - | x::xs when not grab -> - if c_start x then aux (a,s,b) true (x::xs) - else aux (x::a,s,b) grab xs - | x::xs -> - if c_stop x then a, x::s, xs - else aux (a,x::s,b) grab xs in - let a, stack, b = aux ([],[],[]) false s.stack in - s.stack <- List.rev stack; - s.context <- Some (List.rev a, b) - -let unfocus = function - | { context = None } -> raise (Invalid_argument "CStack.unfocus") - | { context = Some (a,b); stack } as s -> - s.context <- None; - s.stack <- a @ stack @ b - -let focused { context } = context <> None - + +let context d = + let top, _, bot = to_lists d in + let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in + List.map (flat pair true) top, List.map (flat pair true) bot + +let iter d f = + let a, s, b = to_lists d in + List.iter (flat f false) a; + List.iter (flat f true) s; + List.iter (flat f false) b + +let stateid_opt_equal = Option.equal Stateid.equal + +let is_in_focus d id = + let _, focused, _ = to_lists d in + List.exists (fun { state_id } -> stateid_opt_equal state_id (Some id)) focused + +let clear d = d.stack <- []; d.context <- None + +let print d f = + let top, mid, bot = to_lists d in + let open Pp in + v 0 + (List.fold_right (fun i acc -> acc ++ cut() ++ flat f false i) top + (List.fold_right (fun i acc -> acc ++ cut() ++ flat f true i) mid + (List.fold_right (fun i acc -> acc ++ cut() ++ flat f false i) bot (mt())))) + +let assign_tip_id d id = + match d with + | { stack = { state_id = None } as top :: _ } -> top.state_id <- Some id + | _ -> invalid_arg "assign_tip_id" + +let cut_at d id = + let aux (n, zone) { state_id; data } = + if stateid_opt_equal state_id (Some id) then CSig.Stop (n, List.rev zone) + else CSig.Cont (n + 1, data :: zone) in + let n, zone = CList.fold_left_until aux (0, []) d.stack in + for i = 1 to n do ignore(pop d) done; + zone + +let find_id d f = + let top, focus, bot = to_lists d in + let pred = function + | { state_id = Some id; data } when f id data -> Some id + | _ -> None in + try CList.find_map pred top, true with Not_found -> + try CList.find_map pred focus, focused d with Not_found -> + CList.find_map pred bot, true + +let before_tip d = + let _, focused, rest = to_lists d in + match focused with + | _:: { state_id = Some id } :: _ -> id, false + | _:: { state_id = None } :: _ -> assert false + | [] -> raise Not_found + | [_] -> + match rest with + | { state_id = Some id } :: _ -> id, true + | { state_id = None } :: _ -> assert false + | [] -> raise Not_found + +let fold_all d a f = + let top, focused, bot = to_lists d in + let a = List.fold_left (fun a -> flat (f a) false) a top in + let a = List.fold_left (fun a -> flat (f a) true) a focused in + let a = List.fold_left (fun a -> flat (f a) false) a bot in + a diff --git a/ide/document.mli b/ide/document.mli index c610f275c..556e1d022 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -6,77 +6,101 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Based on OCaml stacks, it is the structure used by CoqIDE to represent - the document *) - -type 'a t +(* An 'a document is a structure to hold and manipulate list of sentences. + Sentences are equipped with an id = Stateid.t and can carry arbitrary + data ('a). + + When added (push) to the document, a sentence has no id, it has + be manually assigned just afterward or the sentence has to be removed + (pop) before any other sentence can be pushed. + This exception is useful since the process of assigning an id to + a sentence may fail (parse error) and an error handler may want to annotate + a script buffer with the error message. This handler needs to find the + sentence in question, and it is simpler if the sentence is in the document. + Only the functions pop, find, fold_all and find_map can be called on a + document with a tip that has no id (and assign_tip_id of course). + + The document can be focused (non recursively) to a zone. After that + some functions operate on the focused zone only. When unfocused the + context (the part of the document out of focus) is restored. +*) exception Empty -(** Alias for Stack.Empty. *) - -val create : unit -> 'a t -(** Create an empty stack. *) -val push : 'a -> 'a t -> unit -(** Add an element to a stack. *) +type 'a document +type id = Stateid.t -val find : ('a -> bool -> bool) -> 'a t -> 'a -(** Find the first element satisfying the predicate. - The boolean tells If the element is inside the focused zone. - @raise Not_found it there is none. *) +val create : unit -> 'a document -val is_empty : 'a t -> bool -(** Whether a stack is empty. *) +(* Functions that work on the focused part of the document ******************* *) -val iter : ('a -> bool -> unit) -> 'a t -> unit -(** Iterate a function over elements, from the last added one. - The boolean tells If the element is inside the focused zone. *) +(** The last sentence. @raise Invalid_argument if tip has no id. @raise Empty *) +val tip : 'a document -> id -val clear : 'a t -> unit -(** Empty a stack. *) +(** The last sentence. @raise Empty *) +val tip_data : 'a document -> 'a -val length : 'a t -> int -(** Length of a stack. *) +(** Add a sentence on the top (with no state_id) *) +val push : 'a document -> 'a -> unit -val pop : 'a t -> 'a -(** Remove and returns the first element of the stack. - @raise Empty if empty. *) +(** Remove the tip setence. @raise Empty *) +val pop : 'a document -> 'a -val tip : 'a t -> 'a -(** Remove the first element of the stack without modifying it. - @raise Empty if empty. *) +(** Assign the state_id of the tip. @raise Empty *) +val assign_tip_id : 'a document -> id -> unit -val to_list : 'a t -> 'a list -(** Convert to a list. *) +(** [cut_at d id] cuts the document at [id] that is the new tip. + Returns the list of sentences that were cut. + @raise Not_found *) +val cut_at : 'a document -> id -> 'a list -val find_map : ('a -> bool -> 'b option) -> 'a t -> 'b -(** Find the first element that returns [Some _]. - The boolean tells If the element is inside the focused zone. - @raise Not_found it there is none. *) +(* Functions that work on the whole document ********************************* *) -type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c +(** returns the id of the topmost sentence validating the predicate and + a boolean that is true if one needs to unfocus the document to access + such sentence. @raise Not_found *) +val find_id : 'a document -> (id -> 'a -> bool) -> id * bool -(** [seek f acc s] acts like [List.fold_left f acc s] while [f] returns - [Next acc']; it stops returning [b] as soon as [f] returns [Stop b]. - The stack is traversed from the top and is not altered. - @raise Not_found it there is none. *) -val fold_until : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b +(** look for a sentence validating the predicate. The boolean is true + if the sentence is in the zone currently focused. @raise Not_found *) +val find : 'a document -> (bool -> id option -> 'a -> bool) -> 'a +val find_map : 'a document -> (bool -> id option -> 'a -> 'b option) -> 'b (** After [focus s c1 c2] the top of [s] is the topmost element [x] such that [c1 x] is [true] and the bottom is the first element [y] following [x] - such that [c2 y] is [true]. After a focus push/pop/top/fold_until - only use the focused part. - @raise Invalid_argument "CStack.focus" if there is no such [x] and [y] *) -val focus : 'a t -> cond_top:('a -> bool) -> cond_bot:('a -> bool) -> unit + such that [c2 y] is [true]. + @raise Invalid_argument if there is no such [x] and [y] or already focused *) +val focus : + 'a document -> + cond_top:(id -> 'a -> bool) -> cond_bot:(id -> 'a -> bool) -> unit (** Undoes a [focus]. @raise Invalid_argument "CStack.unfocus" if the stack is not focused *) -val unfocus : 'a t -> unit +val unfocus : 'a document -> unit + +(** Is the document focused *) +val focused : 'a document -> bool + +(** No sentences at all *) +val is_empty : 'a document -> bool + +(** returns the 1 to-last sentence, and true if we need to unfocus to reach it. + @raise Not_found *) +val before_tip : 'a document -> id * bool + +(** Is the id in the focused zone? *) +val is_in_focus : 'a document -> id -> bool + +(** Folds over the whole document starting from the topmost (maybe unfocused) + sentence. *) +val fold_all : + 'a document -> 'c -> ('c -> bool -> id option -> 'a -> 'c) -> 'c -(** Is the stack focused *) -val focused : 'a t -> bool +(** Returns (top,bot) such that the document is morally (top @ s @ bot) where + s is the focused part. @raise Invalid_argument *) +val context : 'a document -> (id * 'a) list * (id * 'a) list -(** Returns [top, s, bot] where [top @ s @ bot] is the full stack, and [s] - the focused part *) -val to_lists : 'a t -> 'a list * 'a list * 'a list +(** debug print *) +val print : + 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds |