snapshot, notably:

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 6e57c2e8ffd7614eb280330a8aaa249ac2f198cd..40f2077cfccb3f8a0f8d1f4a0061cab7e859a79d 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -51,8 +51,7 @@ let disambiguator =
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
 
-let currentProof = new MatitaProof.currentProof
-
+let currentProof = MatitaProof.instance ()
 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
 let sequents_viewer =
   let set_goal goal =
@@ -83,15 +82,10 @@ let _ = (* attach observers to proof status *)
     false);
   currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
 
-let currentProof = (currentProof :> MatitaTypes.currentProof)
-let mathViewer =
-  MatitaMathView.mathViewer ~disambiguator
-    ~currentProof:(currentProof :> MatitaTypes.currentProof) ()
+let mathViewer = MatitaMathView.mathViewer ~disambiguator ()
 let interpreter =
-  let console = (gui#console :> MatitaTypes.console) in
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof)
-    ~console ~mathViewer ~dbd ()
+  let console = gui#console in
+  MatitaInterpreter.interpreter ~disambiguator ~console ~mathViewer ()
 let _ =
   let href_callback uri =
     let term = CicAst.Uri (UriManager.string_of_uri uri, None) in
@@ -159,8 +153,7 @@ let _ =
           "Don't know what to do with file: %s\nUnrecognized file format."
           f)));
   ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
-    let currentProof = (currentProof :> MatitaTypes.currentProof) in
-    ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())));
+    ignore (MatitaMathView.cicBrowser ~disambiguator ())));
   connect_button gui#script#scriptWinForwardButton script_forward;
   connect_button gui#script#scriptWinBackButton script_back;
   connect_button gui#script#scriptWinJumpButton script_jump;
@@ -226,9 +219,14 @@ let _ =
     load_script Sys.argv.(1)
   with Invalid_argument _ -> ());
 *)
-  if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin
-    ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())
-  end else begin
+  if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin (* cicbrowser *)
+    let browser = MatitaMathView.cicBrowser ~disambiguator () in
+    Helm_registry.set "matita.mode" "cicbrowser";
+    try
+      browser#loadUri Sys.argv.(1)
+    with Invalid_argument _ -> ()
+  end else begin  (* matita *)
+    Helm_registry.set "matita.mode" "matita";
     gui#main#mainWin#show ();
     gui#toolbar#toolBarWin#show ();
     gui#console#show ()