diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 5 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.opam | 19 | ||||
| -rw-r--r-- | ide/coqide_QUARTZ.ml.in | 37 | ||||
| -rw-r--r-- | ide/coqide_WIN32.ml.in | 50 | ||||
| -rw-r--r-- | ide/coqide_X11.ml.in | 11 | ||||
| -rw-r--r-- | ide/coqide_main.ml (renamed from ide/coqide_main.ml4) | 84 | ||||
| -rw-r--r-- | ide/coqide_os_specific.mli | 11 | ||||
| -rw-r--r-- | ide/dune | 42 | ||||
| -rw-r--r-- | ide/dune-project | 3 | ||||
| -rw-r--r-- | ide/fake_ide.ml | 334 | ||||
| -rw-r--r-- | ide/nanoPG.ml | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 27 | ||||
| -rw-r--r-- | ide/protocol/dune | 2 | ||||
| -rw-r--r-- | ide/protocol/xml_lexer.mll | 5 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 8 |
16 files changed, 505 insertions, 137 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index e948360191..88ffb4f0b7 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -42,14 +42,11 @@ let version () = "The Coq Proof Assistant, version %s (%s)\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ - \nThis is %s (%s is the best one for this architecture and OS)\ - \n" + \nThis is %s \n" ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (Filename.basename Sys.executable_name) - Coq_config.best - (** * Initial checks by launching test coqtop processes *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 00d43e6e64..4190f43680 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -769,7 +769,7 @@ let coqtop_arguments sn = let box = dialog#action_area in let ok = GButton.button ~stock:`OK ~packing:box#add () in let ok_cb () = - let nargs = CString.split ' ' entry#text in + let nargs = String.split_on_char ' ' entry#text in if nargs <> args then let failed = Coq.filter_coq_opts nargs in match failed with diff --git a/ide/coqide.opam b/ide/coqide.opam deleted file mode 100644 index ba05b9edcf..0000000000 --- a/ide/coqide.opam +++ /dev/null @@ -1,19 +0,0 @@ -opam-version: "1.2" -maintainer: "The Coq development team <coqdev@inria.fr>" -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.02.3"] - -depends: [ - "dune" { build } - "ocamlfind" { build } - "num" - "camlp5" - "coq" -] - -build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in new file mode 100644 index 0000000000..a08bac5772 --- /dev/null +++ b/ide/coqide_QUARTZ.ml.in @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let osx = GosxApplication.osxapplication () + +let () = + let _ = osx#connect#ns_application_open_file + ~callback:(fun x -> Coqide.do_load x; true) + in + let _ = osx#connect#ns_application_block_termination + ~callback:Coqide.forbid_quit + in + let _ = osx#connect#ns_application_will_terminate + ~callback:Coqide.close_and_quit + in () + +let init () = + let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication + (GtkMenu.MenuShell.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) + in + let () = GtkosxApplication.Application.insert_app_menu_item + osx#as_osxapplication + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 + in + let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication + (Some (GtkMenu.MenuItem.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) + in + osx#ready () diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in new file mode 100644 index 0000000000..8c4649fc39 --- /dev/null +++ b/ide/coqide_WIN32.ml.in @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* On win32, we add the directory of coqide to the PATH at launch-time + (this used to be done in a .bat script). *) + +let set_win32_path () = + Unix.putenv "PATH" + (Filename.dirname Sys.executable_name ^ ";" ^ + (try Sys.getenv "PATH" with _ -> "")) + +(* On win32, since coqide is now console-free, we re-route stdout/stderr + to avoid Sys_error if someone writes to them. We write to a pipe which + is never read (by default) or to a temp log file (when in debug mode). +*) + +let reroute_stdout_stderr () = + (* We anticipate a bit the argument parsing and look for -debug *) + let debug = List.mem "-debug" (Array.to_list Sys.argv) in + Minilib.debug := debug; + let out_descr = + if debug then + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + Unix.descr_of_out_channel chan + else + snd (Unix.pipe ()) + in + Unix.set_close_on_exec out_descr; + Unix.dup2 out_descr Unix.stdout; + Unix.dup2 out_descr Unix.stderr + +(* We also provide specific kill and interrupt functions. *) + +external win32_kill : int -> unit = "win32_kill" +external win32_interrupt : int -> unit = "win32_interrupt" +let () = + Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; + set_win32_path (); + Coq.interrupter := win32_interrupt; + reroute_stdout_stderr () + +let init () = () diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in new file mode 100644 index 0000000000..6a5784eac3 --- /dev/null +++ b/ide/coqide_X11.ml.in @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let init () = () diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml index 3a92e1bc91..91e8be875a 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml @@ -49,88 +49,6 @@ let catch_gtk_messages () = let () = catch_gtk_messages () - - -(** System-dependent settings *) - -let os_specific_init () = () - -(** Win32 *) - -IFDEF WIN32 THEN - -(* On win32, we add the directory of coqide to the PATH at launch-time - (this used to be done in a .bat script). *) - -let set_win32_path () = - Unix.putenv "PATH" - (Filename.dirname Sys.executable_name ^ ";" ^ - (try Sys.getenv "PATH" with _ -> "")) - -(* On win32, since coqide is now console-free, we re-route stdout/stderr - to avoid Sys_error if someone writes to them. We write to a pipe which - is never read (by default) or to a temp log file (when in debug mode). -*) - -let reroute_stdout_stderr () = - (* We anticipate a bit the argument parsing and look for -debug *) - let debug = List.mem "-debug" (Array.to_list Sys.argv) in - Minilib.debug := debug; - let out_descr = - if debug then - let (name,chan) = Filename.open_temp_file "coqide_" ".log" in - Coqide.logfile := Some name; - Unix.descr_of_out_channel chan - else - snd (Unix.pipe ()) - in - Unix.set_close_on_exec out_descr; - Unix.dup2 out_descr Unix.stdout; - Unix.dup2 out_descr Unix.stderr - -(* We also provide specific kill and interrupt functions. *) - -external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" -let () = - Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; - set_win32_path (); - Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () -END - -(** MacOSX *) - -IFDEF QUARTZ THEN -let osx = GosxApplication.osxapplication () - -let () = - let _ = osx#connect#ns_application_open_file - ~callback:(fun x -> Coqide.do_load x; true) - in - let _ = osx#connect#ns_application_block_termination - ~callback:Coqide.forbid_quit - in - let _ = osx#connect#ns_application_will_terminate - ~callback:Coqide.close_and_quit - in () - -let os_specific_init () = - let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication - (GtkMenu.MenuShell.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) - in - let () = GtkosxApplication.Application.insert_app_menu_item - osx#as_osxapplication - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 - in - let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication - (Some (GtkMenu.MenuItem.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) - in - osx#ready () -END - let load_prefs () = try Preferences.load_pref () with e -> Ideutils.flash_info @@ -145,7 +63,7 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - os_specific_init (); + Coqide_os_specific.init (); try GMain.main (); failwith "Gtk loop ended" diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli new file mode 100644 index 0000000000..ebd09099f0 --- /dev/null +++ b/ide/coqide_os_specific.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val init : unit -> unit @@ -1,21 +1,45 @@ +; IDE Server +(ocamllex utf8_convert config_lexer coq_lex) + +(library + (name core) + (public_name coqide-server.core) + (wrapped false) + (modules document) + (libraries coq.lib)) + +(executable + (name fake_ide) + (public_name fake_ide) + (package coqide-server) + (modules fake_ide) + (libraries coqide-server.protocol coqide-server.core)) + (executable (name idetop) (public_name coqidetop.opt) - (package coqide) + (package coqide-server) (modules idetop) - (libraries coq.toplevel coqide.protocol) + (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) - (deps (:ml4-file coqide_main.ml4)) - (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + (targets coqide_os_specific.ml) + (deps (:in-file coqide_X11.ml.in)) ; TODO support others + (action (run cp %{in-file} %{targets}))) (executable (name coqide_main) (public_name coqide) (package coqide) - (modules (:standard \ idetop)) - (libraries threads str lablgtk2.sourceview2 coq.lib coqide.protocol)) - -(ocamllex utf8_convert config_lexer coq_lex) + (modules coqide_main) + (libraries coqide.gui)) diff --git a/ide/dune-project b/ide/dune-project deleted file mode 100644 index 948dc59000..0000000000 --- a/ide/dune-project +++ /dev/null @@ -1,3 +0,0 @@ -(lang dune 1.0) - -(name coqide-devel) 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *) + +let error s = + prerr_endline ("fake_id: error: "^s); + exit 1 + +let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp + +type coqtop = { + xml_printer : Xml_printer.t; + xml_parser : Xml_parser.t; +} + +let print_error msg = + Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg + +let base_eval_call ?(print=true) ?(fail=true) call coqtop = + if print then prerr_endline (Xmlprotocol.pr_call call); + let xml_query = Xmlprotocol.of_call call in + Xml_printer.print coqtop.xml_printer xml_query; + let rec loop () = + let xml = Xml_parser.parse coqtop.xml_parser in + if Xmlprotocol.is_feedback xml then + loop () + else Xmlprotocol.to_answer call xml + in + let res = loop () in + if print then prerr_endline (Xmlprotocol.pr_full_value call res); + match res with + | Interface.Fail (_,_,s) when fail -> 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|-) [<coqtop>]\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/nanoPG.ml b/ide/nanoPG.ml index 2be5dce426..002722ace9 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -189,7 +189,7 @@ let emacs = insert emacs "Emacs" [] [ run "Edit" "Cut"; { s with kill = Some(txt,false); sel = false } else s)); - mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> + mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in let k = if i#ends_line then begin diff --git a/ide/preferences.ml b/ide/preferences.ml index 955ee87840..6dc922c225 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -167,7 +167,7 @@ object method into l = try Some (CList.map (fun s -> - let split = CString.split sep s in + let split = String.split_on_char sep s in CList.nth split 0, CList.nth split 1) l) with Failure _ -> None end @@ -345,8 +345,15 @@ let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" let modifiers_valid = new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string) +let browser_cmd_fmt = + try + let coq_netscape_remote_var = "COQREMOTEBROWSER" in + Sys.getenv coq_netscape_remote_var + with + Not_found -> Coq_config.browser + let cmd_browse = - new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string) + new preference ~name:["cmd_browse"] ~init:browser_cmd_fmt ~repr:Repr.(string) let cmd_editor = let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in @@ -359,6 +366,14 @@ let text_font = in new preference ~name:["text_font"] ~init ~repr:Repr.(string) +let is_standard_doc_url url = + let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in + let n = String.length Coq_config.wwwcoq in + let n' = String.length Coq_config.wwwrefman in + url = Coq_config.localwwwrefman || + url = Coq_config.wwwrefman || + url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) + let doc_url = object inherit [string] preference @@ -366,7 +381,7 @@ object as super method! set v = - if not (Flags.is_standard_doc_url v) && + if not (is_standard_doc_url v) && v <> use_default_doc_url && (* Extra hack to support links to last released doc version *) v <> Coq_config.wwwcoq ^ "doc" && @@ -673,10 +688,6 @@ let pmodifiers ?(all = false) name p = modifiers name (str_to_mod_list p#get) -[@@@ocaml.warning "-3"] (* String.uppercase_ascii since 4.03.0 GPR#124 *) -let uppercase = String.uppercase -[@@@ocaml.warning "+3"] - let configure ?(apply=(fun () -> ())) () = let cmd_coqtop = string @@ -1003,7 +1014,7 @@ let configure ?(apply=(fun () -> ())) () = let k = if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k else "" in - let k = uppercase k in + let k = String.uppercase_ascii k in [q, k] in 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/ide/protocol/xml_lexer.mll b/ide/protocol/xml_lexer.mll index 4a52147e17..e8bf7e16ae 100644 --- a/ide/protocol/xml_lexer.mll +++ b/ide/protocol/xml_lexer.mll @@ -83,9 +83,6 @@ let error lexbuf e = last_pos := lexeme_start lexbuf; raise (Error e) -[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *) -let lowercase = String.lowercase -[@@@ocaml.warning "+3"] } let newline = ['\n'] @@ -222,7 +219,7 @@ and entity = parse { let ident = lexeme lexbuf in try - Hashtbl.find idents (lowercase ident) + Hashtbl.find idents (String.lowercase_ascii ident) with Not_found -> "&" ^ ident } diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 8eddfb3149..06281d6287 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -98,7 +98,7 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let result = Wg_MessageView.message_view () in router#register_route route_id result; - r_bin#add (result :> GObj.widget); + r_bin#add_with_viewport (result :> GObj.widget); views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in @@ -152,9 +152,9 @@ object(self) method show = frame#show; let cur_page = notebook#get_nth_page notebook#current_page in - let _, _, e = - List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in - e#misc#grab_focus () + match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with + | (_, _, e) -> e#misc#grab_focus () + | exception Not_found -> () method hide = frame#hide |