diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqmktop.ml | 2 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 36 |
2 files changed, 29 insertions, 9 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 81f0686e02..39a8ede9a9 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -30,7 +30,7 @@ let safe_sys_command = cf. dev/dynlink.ml. *) (* 1. Core objects *) -let ocamlobjs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma"] +let ocamlobjs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] let camlp4objs = if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"] let libobjs = ocamlobjs @ camlp4objs diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 14499c2280..5bfa377f0b 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -11,14 +11,13 @@ exception Comment type coqtop = { - in_chan : in_channel; xml_printer : Xml_printer.t; xml_parser : Xml_parser.t; } let logger level content = () -let eval_call call coqtop = +let base_eval_call call coqtop = prerr_endline (Serialize.pr_call call); let xml_query = Serialize.of_call call in Xml_printer.print coqtop.xml_printer xml_query; @@ -36,18 +35,40 @@ let eval_call call coqtop = in let res = loop () in prerr_endline (Serialize.pr_full_value call res); - match res with Interface.Fail _ -> exit 1 | _ -> () + match res with Interface.Fail _ -> exit 1 | x -> x + +let eval_call c q = ignore(base_eval_call c q) + +let ids = ref [] +let store_id = function + | Interface.Fail _ -> () + | Interface.Good (id, _) -> ids := id :: !ids +let rec erase_ids n = + if n = 0 then + match !ids with + | [] -> Stateid.initial_state_id + | x :: _ -> x + else match !ids with + | id :: rest -> ids := rest; erase_ids (n-1) + | [] -> exit 1 +let eid = ref 0 +let edit () = incr eid; !eid let commands = [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (0,true,false,s))); "INTERPRAW", (fun s -> eval_call (Serialize.interp (0,true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Serialize.interp (0,false,false,s))); - "INTERP", (fun s -> eval_call (Serialize.interp (0,false,true,s))); - "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s))); + "INTERPSILENT", (fun s c -> + store_id (base_eval_call (Serialize.interp (edit(),false,false,s)) c)); + "INTERP", (fun s c -> + store_id (base_eval_call (Serialize.interp (edit(),false,true,s)) c)); + "REWIND", (fun s -> + let i = int_of_string s in + let id = erase_ids i in + eval_call (Serialize.backto id)); "GOALS", (fun _ -> eval_call (Serialize.goals ())); "HINTS", (fun _ -> eval_call (Serialize.hints ())); "GETOPTIONS", (fun _ -> eval_call (Serialize.get_options ())); - "STATUS", (fun _ -> eval_call (Serialize.status ())); + "STATUS", (fun _ -> eval_call (Serialize.status false)); "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s)); "MKCASES", (fun s -> eval_call (Serialize.mkcases s)); "#", (fun _ -> raise Comment); @@ -91,7 +112,6 @@ let main = let op = Xml_printer.make (Xml_printer.TChannel cout) in let () = Xml_parser.check_eof ip false in { - in_chan = cin; xml_printer = op; xml_parser = ip; } |