diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:53:05 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:53:05 +0000 |
| commit | bab9baefceedda169095ddcc16df47d35b2f6af3 (patch) | |
| tree | 5652faa8dfcf8e885a30fed07b7b7c17b264d679 /toplevel/coqtop.ml | |
| parent | c81254903e1e50a2305cd48ccfb673d9737afc48 (diff) | |
stm: (initial) support for -coq-slaves
Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 394cce6ce..26e3081bb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -302,6 +302,14 @@ let parse_args arglist = Flags.make_term_color false; parse ("-emacs" :: rem) + | "-coq-slaves" :: "off" :: rem -> Flags.coq_slave_mode := -1; parse rem + | "-coq-slaves" :: "on" :: rem -> Flags.coq_slave_mode := 0; parse rem + + | "-coq-slaves" :: n :: rem -> (* internal use *) + assert (int_of_string n > 0); + Flags.coq_slave_mode := int_of_string n; + parse rem + | "-unicode" :: rem -> add_require "Utf8_core"; parse rem | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem @@ -374,6 +382,9 @@ let init arglist = if !Flags.ide_slave then begin Flags.make_silent true; Ide_slave.init_stdout () + end else if !Flags.coq_slave_mode > 0 then begin + Flags.make_silent true; + Stm.slave_init_stdout () end; if_verbose print_header (); init_load_path (); @@ -421,6 +432,8 @@ let start () = Dumpglob.noglob () in if !Flags.ide_slave then Ide_slave.loop () + else if !Flags.coq_slave_mode > 0 then + Stm.slave_main_loop () else Toplevel.loop(); (* Initialise and launch the Ocaml toplevel *) |