From faf6ffc00d91a7cc759ef65f9864d00773c96b19 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 3 Oct 2018 20:54:32 +0200 Subject: [ide] [dune] [test-suite] Reorganize `fake_ide` build. Even if `fake_ide` was under tools, it depended on libraries from `ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the test-suite [this means `test-suite` depends on the `ide` folder then]. In the Dune side, we reorganize libraries so `fake_ide` doesn't depend on GTK anymore, this allows to run the test-suite when GTK is not available. In order to achieve this, we had to split the `coqide` package in a server and client version. --- .gitlab-ci.yml | 1 + Makefile.build | 4 +- coqide-server.opam | 16 +++ coqide.opam | 1 + ide/dune | 39 +++++-- ide/fake_ide.ml | 334 +++++++++++++++++++++++++++++++++++++++++++++++++++++ ide/protocol/dune | 2 +- tools/fake_ide.ml | 334 ----------------------------------------------------- 8 files changed, 382 insertions(+), 349 deletions(-) create mode 100644 coqide-server.opam create mode 100644 ide/fake_ide.ml delete mode 100644 tools/fake_ide.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 18f515da24..ef7caa98d4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -241,6 +241,7 @@ pkg:opam: script: - set -e - opam pin add coq . + - opam pin add coqide-server . - opam pin add coqide . - set +e variables: diff --git a/Makefile.build b/Makefile.build index 0faa18b059..ee758fcc5f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -563,7 +563,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqidetop -FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo +FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP) $(SHOW)'OCAMLBEST -o $@' @@ -668,7 +668,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib $(SHOW)'OCAMLOPT -pack -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,) +COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,) COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,) COND_BYTEFLAGS= \ diff --git a/coqide-server.opam b/coqide-server.opam new file mode 100644 index 0000000000..546ce75dbd --- /dev/null +++ b/coqide-server.opam @@ -0,0 +1,16 @@ +opam-version: "1.2" +maintainer: "The Coq development team " +authors: "The Coq development team, INRIA, CNRS, and contributors." +homepage: "https://coq.inria.fr/" +bug-reports: "https://github.com/coq/coq/issues" +dev-repo: "https://github.com/coq/coq.git" +license: "LGPL-2.1" + +available: [ocaml-version >= "4.05.0"] + +depends: [ + "dune" { build & >= "1.2.0" } + "coq" +] + +build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coqide.opam b/coqide.opam index 897177b283..17fb5dbbe2 100644 --- a/coqide.opam +++ b/coqide.opam @@ -11,6 +11,7 @@ available: [ocaml-version >= "4.05.0"] depends: [ "dune" { build & >= "1.2.0" } "coq" + "coqide-server" "conf-gtksourceview" "lablgtk" { >= "2.18.5" } ] diff --git a/ide/dune b/ide/dune index 6931a747ac..037b0fcc9e 100644 --- a/ide/dune +++ b/ide/dune @@ -1,11 +1,34 @@ +; IDE Server (ocamllex utf8_convert config_lexer coq_lex) (library (name core) - (public_name coqide.core) + (public_name coqide-server.core) (wrapped false) - (modules (:standard \ idetop coqide_main)) - (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol)) + (modules document) + (libraries coq.lib)) + +(executable + (name fake_ide) + (modules fake_ide) + (libraries coqide-server.protocol coqide-server.core)) + +(executable + (name idetop) + (public_name coqidetop.opt) + (package coqide-server) + (modules idetop) + (libraries coq.toplevel coqide-server.protocol) + (link_flags -linkall)) + +; IDE Client +(library + (name gui) + (public_name coqide.gui) + (wrapped false) + (modules (:standard \ document fake_ide idetop coqide_main)) + (optional) + (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) (rule (targets coqide_main.ml) @@ -17,12 +40,4 @@ (public_name coqide) (package coqide) (modules coqide_main) - (libraries coqide.core)) - -(executable - (name idetop) - (public_name coqidetop.opt) - (package coqide) - (modules idetop) - (libraries coq.toplevel coqide.protocol) - (link_flags -linkall)) + (libraries coqide.gui)) diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml new file mode 100644 index 0000000000..521aff6bf6 --- /dev/null +++ b/ide/fake_ide.ml @@ -0,0 +1,334 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* print_error s; exit 1 + | Interface.Fail (_,_,s) as x -> print_error s; x + | x -> x + +let eval_call c q = ignore(base_eval_call c q) + +module Parser = struct (* {{{ *) + + exception Err of string + exception More + + type token = + | Tok of string * string + | Top of token list + + type grammar = + | Alt of grammar list + | Seq of grammar list + | Opt of grammar + | Item of (string * (string -> token * int)) + + let eat_rex x = x, fun s -> + if Str.string_match (Str.regexp x) s 0 then begin + let m = Str.match_end () in + let w = String.sub s 0 m in + Tok(x,w), m + end else raise (Err ("Regexp "^x^" not found in: "^s)) + + let eat_balanced c = + let c' = match c with + | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in + let sc, sc' = String.make 1 c, String.make 1 c' in + let name = sc ^ "..." ^ sc' in + let unescape s = + Str.global_replace (Str.regexp ("\\\\"^sc)) sc + (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in + name, fun s -> + if s.[0] = c then + let rec find n m = + if String.length s <= m then raise More; + if s.[m] = c' then + if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1 + else find (n-1) (m+1) + else if s.[m] = c then find (n+1) (m+1) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then + find n (m+2) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then + find n (m+2) + else find n (m+1) + in find ~-1 0 + else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s)) + + let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s + + let s = ref "" + + let parse g ic = + let read_more () = s := !s ^ input_line ic ^ "\n" in + let ensure_non_empty n = if n = String.length !s then read_more () in + let cut_after s n = String.sub s n (String.length s - n) in + let rec wrap f n = + try + ensure_non_empty n; + let _, n' = eat_blanks (cut_after !s n) in + ensure_non_empty n'; + let t, m = f (cut_after !s (n+n')) in + let _, m' = eat_blanks (cut_after !s (n+n'+m)) in + t, n+n'+m+m' + with More -> read_more (); wrap f n in + let rec aux n g res : token list * int = + match g with + | Item (_,f) -> + let t, n = wrap f n in + t :: res, n + | Opt g -> + (try let res', n = aux n g [] in Top (List.rev res') :: res, n + with Err _ -> Top [] :: res, n) + | Alt gl -> + let rec fst = function + | [] -> raise (Err ("No more alternatives for: "^cut_after !s n)) + | g :: gl -> + try aux n g res + with Err s -> fst gl in + fst gl + | Seq gl -> + let rec all (res,n) = function + | [] -> res, n + | g :: gl -> all (aux n g res) gl in + all (res,n) gl in + let res, n = aux 0 g [] in + s := cut_after !s n; + List.rev res + + let clean s = Str.global_replace (Str.regexp "\n") "\\n" s + + let rec print g = + match g with + | Item (s,_) -> Printf.sprintf "%s" (clean s) + | Opt g -> Printf.sprintf "[%s]" (print g) + | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Seq gs -> String.concat " " (List.map print gs) + + let rec print_toklist = function + | [] -> "" + | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest + | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest + | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest + +end (* }}} *) + +type sentence = { + name : string; + text : string; + edit_id : int; +} + +let doc : sentence Document.document = Document.create () + +let tip_id () = + try Document.tip doc + with + | Document.Empty -> Stateid.initial + | Invalid_argument _ -> error "add_sentence on top of non assigned tip" + +let add_sentence = + let edit_id = ref 0 in + fun ?(name="") text -> + let tip_id = tip_id () in + decr edit_id; + Document.push doc { name; text; edit_id = !edit_id }; + !edit_id, tip_id + +let print_document () = + let ellipsize s = + Str.global_replace (Str.regexp "^[\n ]*") "" + (if String.length s > 20 then String.sub s 0 17 ^ "..." + else s) in + pperr_endline ( + (Document.print doc + (fun b state_id { name; text } -> + Pp.str (Printf.sprintf "%s[%10s, %3s] %s" + (if b then "*" else " ") + name + (Stateid.to_string (Option.default Stateid.dummy state_id)) + (ellipsize text))))) + +(* This module is the logic a GUI has to implement *) +module GUILogic = struct + + let after_add = function + | Interface.Fail (_,_,s) -> print_error s; exit 1 + | Interface.Good (id, (Util.Inl (), _)) -> + Document.assign_tip_id doc id + | Interface.Good (id, (Util.Inr tip, _)) -> + Document.assign_tip_id doc id; + Document.unfocus doc; + ignore(Document.cut_at doc tip); + print_document () + + let at id id' _ = Stateid.equal id' id + + let after_edit_at (id,need_unfocus) = function + | Interface.Fail (_,_,s) -> print_error s; exit 1 + | Interface.Good (Util.Inl ()) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc id); + print_document () + | Interface.Good (Util.Inr (stop_id,(start_id,tip))) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc tip); + Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id); + ignore(Document.cut_at doc id); + print_document () + + let get_id_pred pred = + try Document.find_id doc pred + with Not_found -> error "No state found" + + let get_id id = get_id_pred (fun _ { name } -> name = id) + + let after_fail coq = function + | Interface.Fail (safe_id,_,s) -> + prerr_endline "The command failed as expected"; + let to_id, need_unfocus = + get_id_pred (fun id _ -> Stateid.equal id safe_id) in + after_edit_at (to_id, need_unfocus) + (base_eval_call (Xmlprotocol.edit_at to_id) coq) + | Interface.Good _ -> error "The command was expected to fail but did not" + +end + +open GUILogic + +let eval_print l coq = + let open Parser in + let open Xmlprotocol in + (* prerr_endline ("Interpreting: " ^ print_toklist l); *) + match l with + | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] -> + let eid, tip = add_sentence phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> + let eid, tip = add_sentence ~name phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"GOALS"); ] -> + eval_call (goals ()) coq + | [ Tok(_,"FAILGOALS"); ] -> + after_fail coq (base_eval_call ~fail:false (goals ()) coq) + | [ Tok(_,"EDIT_AT"); Tok(_,id) ] -> + let to_id, need_unfocus = get_id id in + after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) + | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> + eval_call (query (0,(phrase,tip_id()))) coq + | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> + let to_id, _ = get_id id in + eval_call (query (0,(phrase, to_id))) coq + | [ Tok(_,"WAIT") ] -> + eval_call (wait ()) coq + | [ Tok(_,"JOIN") ] -> + eval_call (status true) coq + | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> + let to_id, _ = get_id id in + if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" + else prerr_endline "Good tip" + | Tok("#[^\n]*",_) :: _ -> () + | _ -> error "syntax error" + +let grammar = + let open Parser in + let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in + let eat_phrase = eat_balanced '{' in + Alt + [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] + ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "WAIT")] + ; Seq [Item (eat_rex "JOIN")] + ; Seq [Item (eat_rex "GOALS")] + ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] + ; Item (eat_rex "#[^\n]*") + ] + +let read_command inc = Parser.parse grammar inc + +let usage () = + error (Printf.sprintf + "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ + Usage: %s (file|-) []\n\ + Input syntax is the following:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)) + +module Coqide = Spawn.Sync () + +let main = + if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe + (Sys.Signal_handle + (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); + let def_args = ["--xml_format=Ppcmds"] in + let idetop_name = System.get_toplevel_path "coqidetop" in + let coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> Array.of_list def_args, f + | [| _; f; ct |] -> + let ct = Str.split (Str.regexp " ") ct in + Array.of_list (def_args @ ct), f + | _ -> usage () in + let inc = if input_file = "-" then stdin else open_in input_file in + let coq = + let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in + let ip = Xml_parser.make (Xml_parser.SChannel cin) in + let op = Xml_printer.make (Xml_printer.TChannel cout) in + Xml_parser.check_eof ip false; + { xml_printer = op; xml_parser = ip } in + let init () = + match base_eval_call ~print:false (Xmlprotocol.init None) coq with + | Interface.Good id -> + let dir = Filename.dirname input_file in + let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in + let eid, tip = add_sentence ~name:"initial" phrase in + after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Fail _ -> error "init call failed" in + let finish () = + match base_eval_call (Xmlprotocol.status true) coq with + | Interface.Good _ -> exit 0 + | Interface.Fail (_,_,s) -> print_error s; exit 1 in + (* The main loop *) + init (); + while true do + let cmd = try read_command inc with End_of_file -> finish () in + try eval_print cmd coq + with e -> error ("Uncaught exception " ^ Printexc.to_string e) + done + +(* vim:set foldmethod=marker: *) diff --git a/ide/protocol/dune b/ide/protocol/dune index 9ce4559940..801ceb20ec 100644 --- a/ide/protocol/dune +++ b/ide/protocol/dune @@ -1,6 +1,6 @@ (library (name protocol) - (public_name coqide.protocol) + (public_name coqide-server.protocol) (wrapped false) (libraries coq.lib)) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml deleted file mode 100644 index 0162011289..0000000000 --- a/tools/fake_ide.ml +++ /dev/null @@ -1,334 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* print_error s; exit 1 - | Interface.Fail (_,_,s) as x -> print_error s; x - | x -> x - -let eval_call c q = ignore(base_eval_call c q) - -module Parser = struct (* {{{ *) - - exception Err of string - exception More - - type token = - | Tok of string * string - | Top of token list - - type grammar = - | Alt of grammar list - | Seq of grammar list - | Opt of grammar - | Item of (string * (string -> token * int)) - - let eat_rex x = x, fun s -> - if Str.string_match (Str.regexp x) s 0 then begin - let m = Str.match_end () in - let w = String.sub s 0 m in - Tok(x,w), m - end else raise (Err ("Regexp "^x^" not found in: "^s)) - - let eat_balanced c = - let c' = match c with - | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in - let sc, sc' = String.make 1 c, String.make 1 c' in - let name = sc ^ "..." ^ sc' in - let unescape s = - Str.global_replace (Str.regexp ("\\\\"^sc)) sc - (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in - name, fun s -> - if s.[0] = c then - let rec find n m = - if String.length s <= m then raise More; - if s.[m] = c' then - if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1 - else find (n-1) (m+1) - else if s.[m] = c then find (n+1) (m+1) - else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then - find n (m+2) - else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then - find n (m+2) - else find n (m+1) - in find ~-1 0 - else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s)) - - let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s - - let s = ref "" - - let parse g ic = - let read_more () = s := !s ^ input_line ic ^ "\n" in - let ensure_non_empty n = if n = String.length !s then read_more () in - let cut_after s n = String.sub s n (String.length s - n) in - let rec wrap f n = - try - ensure_non_empty n; - let _, n' = eat_blanks (cut_after !s n) in - ensure_non_empty n'; - let t, m = f (cut_after !s (n+n')) in - let _, m' = eat_blanks (cut_after !s (n+n'+m)) in - t, n+n'+m+m' - with More -> read_more (); wrap f n in - let rec aux n g res : token list * int = - match g with - | Item (_,f) -> - let t, n = wrap f n in - t :: res, n - | Opt g -> - (try let res', n = aux n g [] in Top (List.rev res') :: res, n - with Err _ -> Top [] :: res, n) - | Alt gl -> - let rec fst = function - | [] -> raise (Err ("No more alternatives for: "^cut_after !s n)) - | g :: gl -> - try aux n g res - with Err s -> fst gl in - fst gl - | Seq gl -> - let rec all (res,n) = function - | [] -> res, n - | g :: gl -> all (aux n g res) gl in - all (res,n) gl in - let res, n = aux 0 g [] in - s := cut_after !s n; - List.rev res - - let clean s = Str.global_replace (Str.regexp "\n") "\\n" s - - let rec print g = - match g with - | Item (s,_) -> Printf.sprintf "%s" (clean s) - | Opt g -> Printf.sprintf "[%s]" (print g) - | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) - | Seq gs -> String.concat " " (List.map print gs) - - let rec print_toklist = function - | [] -> "" - | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest - | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest - | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest - -end (* }}} *) - -type sentence = { - name : string; - text : string; - edit_id : int; -} - -let doc : sentence Document.document = Document.create () - -let tip_id () = - try Document.tip doc - with - | Document.Empty -> Stateid.initial - | Invalid_argument _ -> error "add_sentence on top of non assigned tip" - -let add_sentence = - let edit_id = ref 0 in - fun ?(name="") text -> - let tip_id = tip_id () in - decr edit_id; - Document.push doc { name; text; edit_id = !edit_id }; - !edit_id, tip_id - -let print_document () = - let ellipsize s = - Str.global_replace (Str.regexp "^[\n ]*") "" - (if String.length s > 20 then String.sub s 0 17 ^ "..." - else s) in - pperr_endline ( - (Document.print doc - (fun b state_id { name; text } -> - Pp.str (Printf.sprintf "%s[%10s, %3s] %s" - (if b then "*" else " ") - name - (Stateid.to_string (Option.default Stateid.dummy state_id)) - (ellipsize text))))) - -(* This module is the logic a GUI has to implement *) -module GUILogic = struct - - let after_add = function - | Interface.Fail (_,_,s) -> print_error s; exit 1 - | Interface.Good (id, (Util.Inl (), _)) -> - Document.assign_tip_id doc id - | Interface.Good (id, (Util.Inr tip, _)) -> - Document.assign_tip_id doc id; - Document.unfocus doc; - ignore(Document.cut_at doc tip); - print_document () - - let at id id' _ = Stateid.equal id' id - - let after_edit_at (id,need_unfocus) = function - | Interface.Fail (_,_,s) -> print_error s; exit 1 - | Interface.Good (Util.Inl ()) -> - if need_unfocus then Document.unfocus doc; - ignore(Document.cut_at doc id); - print_document () - | Interface.Good (Util.Inr (stop_id,(start_id,tip))) -> - if need_unfocus then Document.unfocus doc; - ignore(Document.cut_at doc tip); - Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id); - ignore(Document.cut_at doc id); - print_document () - - let get_id_pred pred = - try Document.find_id doc pred - with Not_found -> error "No state found" - - let get_id id = get_id_pred (fun _ { name } -> name = id) - - let after_fail coq = function - | Interface.Fail (safe_id,_,s) -> - prerr_endline "The command failed as expected"; - let to_id, need_unfocus = - get_id_pred (fun id _ -> Stateid.equal id safe_id) in - after_edit_at (to_id, need_unfocus) - (base_eval_call (Xmlprotocol.edit_at to_id) coq) - | Interface.Good _ -> error "The command was expected to fail but did not" - -end - -open GUILogic - -let eval_print l coq = - let open Parser in - let open Xmlprotocol in - (* prerr_endline ("Interpreting: " ^ print_toklist l); *) - match l with - | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] -> - let eid, tip = add_sentence phrase in - after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) - | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> - let eid, tip = add_sentence ~name phrase in - after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) - | [ Tok(_,"GOALS"); ] -> - eval_call (goals ()) coq - | [ Tok(_,"FAILGOALS"); ] -> - after_fail coq (base_eval_call ~fail:false (goals ()) coq) - | [ Tok(_,"EDIT_AT"); Tok(_,id) ] -> - let to_id, need_unfocus = get_id id in - after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) - | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> - eval_call (query (0,(phrase,tip_id()))) coq - | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> - let to_id, _ = get_id id in - eval_call (query (0,(phrase, to_id))) coq - | [ Tok(_,"WAIT") ] -> - eval_call (wait ()) coq - | [ Tok(_,"JOIN") ] -> - eval_call (status true) coq - | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> - let to_id, _ = get_id id in - if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" - else prerr_endline "Good tip" - | Tok("#[^\n]*",_) :: _ -> () - | _ -> error "syntax error" - -let grammar = - let open Parser in - let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in - let eat_phrase = eat_balanced '{' in - Alt - [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] - ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] - ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] - ; Seq [Item (eat_rex "WAIT")] - ; Seq [Item (eat_rex "JOIN")] - ; Seq [Item (eat_rex "GOALS")] - ; Seq [Item (eat_rex "FAILGOALS")] - ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] - ; Item (eat_rex "#[^\n]*") - ] - -let read_command inc = Parser.parse grammar inc - -let usage () = - error (Printf.sprintf - "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ - Usage: %s (file|-) []\n\ - Input syntax is the following:\n%s\n" - (Filename.basename Sys.argv.(0)) - (Parser.print grammar)) - -module Coqide = Spawn.Sync () - -let main = - if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe - (Sys.Signal_handle - (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"] in - let idetop_name = System.get_toplevel_path "coqidetop" in - let coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> Array.of_list def_args, f - | [| _; f; ct |] -> - let ct = Str.split (Str.regexp " ") ct in - Array.of_list (def_args @ ct), f - | _ -> usage () in - let inc = if input_file = "-" then stdin else open_in input_file in - let coq = - let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in - let ip = Xml_parser.make (Xml_parser.SChannel cin) in - let op = Xml_printer.make (Xml_printer.TChannel cout) in - Xml_parser.check_eof ip false; - { xml_printer = op; xml_parser = ip } in - let init () = - match base_eval_call ~print:false (Xmlprotocol.init None) coq with - | Interface.Good id -> - let dir = Filename.dirname input_file in - let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in - let eid, tip = add_sentence ~name:"initial" phrase in - after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) - | Interface.Fail _ -> error "init call failed" in - let finish () = - match base_eval_call (Xmlprotocol.status true) coq with - | Interface.Good _ -> exit 0 - | Interface.Fail (_,_,s) -> print_error s; exit 1 in - (* The main loop *) - init (); - while true do - let cmd = try read_command inc with End_of_file -> finish () in - try eval_print cmd coq - with e -> error ("Uncaught exception " ^ Printexc.to_string e) - done - -(* vim:set foldmethod=marker: *) -- cgit v1.2.3