diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coq.ml | 13 | ||||
-rw-r--r-- | ide/coq.mli | 4 | ||||
-rw-r--r-- | ide/coqide.ml | 10 |
3 files changed, 15 insertions, 12 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index fecd3f292..cb9d5b895 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -28,11 +28,13 @@ open Compat type coqtop = { mutable cout : in_channel ; mutable cin : out_channel ; + sup_args : string ; } let dummy_coqtop = { cout = stdin ; cin = stdout ; + sup_args = "" ; } let prerr_endline s = if !debug then prerr_endline s else () @@ -47,9 +49,6 @@ let msg m = let msgnl m = (msg m)^"\n" -let init () = List.tl (Array.to_list Sys.argv) -(* Coqtop.init_ide (List.tl (Array.to_list Sys.argv))*) - let i = ref 0 let get_version_date () = @@ -103,17 +102,17 @@ let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i) let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout -let spawn_coqtop () = +let spawn_coqtop sup_args = let prog = Sys.argv.(0) in let dir = Filename.dirname prog in - let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave") in - { cin = ic; cout = oc } + let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave "^sup_args) in + { cin = ic; cout = oc ; sup_args = sup_args } let kill_coqtop coqtop = raw_interp coqtop "Quit." let reset_coqtop coqtop = kill_coqtop coqtop; - let ni = spawn_coqtop () in + let ni = spawn_coqtop coqtop.sup_args in coqtop.cin <- ni.cin; coqtop.cout <- ni.cout diff --git a/ide/coq.mli b/ide/coq.mli index 914eb708a..926919f70 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -19,7 +19,7 @@ type coqtop val dummy_coqtop : coqtop -val spawn_coqtop : unit -> coqtop +val spawn_coqtop : string -> coqtop val kill_coqtop : coqtop -> unit @@ -43,8 +43,6 @@ end val reset_initial : unit -> unit -val init : unit -> string list - val raw_interp : coqtop -> string -> unit val interp : coqtop -> bool -> string -> int diff --git a/ide/coqide.ml b/ide/coqide.ml index e8198ec6f..4266d6fb3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -529,6 +529,8 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) +let sup_args = ref "" + class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct = object(self) val input_view = _script @@ -1361,7 +1363,7 @@ let create_session () = let stack = Stack.create () in let ct = - spawn_coqtop () in + spawn_coqtop !sup_args in let legacy_av = new analyzed_view script proof message stack ct in let _ = @@ -3117,9 +3119,13 @@ let rec check_for_geoproof_input () = (* cb_Dr#set_text "Ack" *) done +let rec init = function + | [] -> [] + | "-args"::str::rem -> sup_args := str; init rem + | f::rem -> f::(init rem) let start () = - let files = Coq.init () in + let files = init (List.tl (Array.to_list Sys.argv)) in ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); (try |