X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=11ae70642bf6b36c5f59e2b644648ca23522c7e7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=59076c94ed540a53c98a99cb6fbdedf8fa3a8498;hpb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 59076c94e..11ae70642 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,47 +23,186 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 open MatitaGtkMisc
+open MatitaTypes
 
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
+(** {2 Initialization} *)
 
-  (** exceptions whose content should be presented to the user *)
-exception Failure of string
-let error s = raise (Failure s)
+let _ = MatitaInit.initialize_all ()
+let _ = Paramodulation.Saturation.init () (* ALB to link paramodulation *)
 
-let _ = Helm_registry.load_from "matita.conf.xml"
-let _ = GMain.Main.init ()
-let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
+(** {2 GUI callbacks} *)
 
-  (** quit program, possibly asking for confirmation *)
-let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ = gui#main#debugMenu#misc#hide ()
+let gui = MatitaGui.instance ()
 
-  (** <DEBUGGING> *)
-if BuildTimeConf.debug then begin
-  gui#main#debugMenu#misc#show ();
-  let addDebugItem ~label callback =
-    let item = GMenu.menu_item ~label () in
-    gui#main#debugMenu_menu#append item;
-    ignore (item#connect#activate callback);
+let script =
+  let s = 
+    MatitaScript.script 
+      ~source_view:gui#sourceView
+      ~init:(Lazy.force MatitaEngine.initial_status) 
+      ~mathviewer:(MatitaMathView.mathViewer ())
+      ~urichooser:(fun uris ->
+        try
+          MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+          ~title:"Matita: URI chooser" 
+          ~msg:"Select the URI" ~hide_uri_entry:true
+          ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+          ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
+          () ~id:"boh?" uris
+        with MatitaTypes.Cancel -> [])
+      ~set_star:gui#setStar
+      ~ask_confirmation:
+        (fun ~title ~message -> 
+            MatitaGtkMisc.ask_confirmation ~title ~message 
+            ~parent:gui#main#toplevel ())
+      ~develcreator:gui#createDevelopment
+      ()
+  in
+  gui#sourceView#source_buffer#begin_not_undoable_action ();
+  s#reset (); 
+  s#template (); 
+  gui#sourceView#source_buffer#end_not_undoable_action ();
+  s
+  
+  (* math viewers *)
+let _ =
+  let cic_math_view = MatitaMathView.cicMathView_instance () in
+  let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
+  sequents_viewer#load_logo;
+  cic_math_view#set_href_callback
+    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load
+      (`Uri (UriManager.uri_of_string uri))));
+  let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+  let sequents_observer status =
+    sequents_viewer#reset;
+    match status.proof_status with
+    | Incomplete_proof ({ stack = stack } as incomplete_proof) ->
+        sequents_viewer#load_sequents incomplete_proof;
+        (try
+          script#setGoal (Continuationals.Stack.find_goal stack);
+          sequents_viewer#goto_sequent script#goal
+        with Failure _ -> script#setGoal ~-1);
+    | Proof proof -> sequents_viewer#load_logo_with_qed
+    | No_proof -> sequents_viewer#load_logo
+    | Intermediate _ -> assert false (* only the engine may be in this state *)
   in
-  addDebugItem "interactive user uri choice" (fun _ ->
-    try
-      let uris =
-        interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
-          ~title:"titolo" ~msg:"messaggio" ~nonvars_button:true
-          ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
-          "cic:/cinque.var"]
+  script#addObserver sequents_observer;
+  script#addObserver browser_observer
+
+  (** {{{ Debugging *)
+let _ =
+  if BuildTimeConf.debug then begin
+    gui#main#debugMenu#misc#show ();
+    let addDebugItem ~label callback =
+      let item =
+        GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
       in
-      List.iter prerr_endline uris
-    with No_choice -> error "no choice");
-  addDebugItem "toggle auto disambiguation" (fun _ ->
-    Helm_registry.set_bool "matita.auto_disambiguation"
-      (not (Helm_registry.get_bool "matita.auto_disambiguation")))
-end
-  (** </DEBUGGING> *)
+      ignore (item#connect#activate callback)
+    in
+    addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+      let oc = open_out "env.dump" in
+      CicEnvironment.dump_to_channel oc;
+      close_out oc);
+    addDebugItem "load environment from \"env.dump\"" (fun _ ->
+      let ic = open_in "env.dump" in
+      CicEnvironment.restore_from_channel ic;
+      close_in ic);
+    addDebugItem "dump universes" (fun _ ->
+      List.iter (fun (u,_,g) -> 
+        prerr_endline (UriManager.string_of_uri u); 
+        CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
+      );
+    addDebugItem "dump environment content" (fun _ ->
+      List.iter (fun (u,_,_) -> 
+        prerr_endline (UriManager.string_of_uri u)) 
+        (CicEnvironment.list_obj ()));
+    addDebugItem "print selections" (fun () ->
+      let cicMathView = MatitaMathView.cicMathView_instance () in
+      List.iter MatitaLog.debug (cicMathView#string_of_selections));
+    addDebugItem "dump script status" script#dump;
+    addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
+      Helm_registry.save_to "./foo.conf.xml");
+    addDebugItem "dump metasenv"
+      (fun _ ->
+         if script#onGoingProof () then
+           MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
+    addDebugItem "dump coercions Db" (fun _ ->
+      List.iter
+        (fun (s,t,u) -> 
+          MatitaLog.debug
+            (UriManager.name_of_uri u ^ ":"
+             ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+        (CoercDb.to_list ()));
+    addDebugItem "print top-level grammar entries"
+      CicNotationParser.print_l2_pattern;
+    addDebugItem "dump moo to stderr" (fun _ ->
+      let status = (MatitaScript.current ())#status in
+      let moo, metadata = status.moo_content_rev in
+      List.iter (fun cmd -> prerr_endline
+        (GrafiteAstPp.pp_command cmd)) (List.rev moo);
+      List.iter (fun m -> prerr_endline
+        (GrafiteAstPp.pp_metadata m)) metadata);
+    addDebugItem "print metasenv goals and stack to stderr"
+      (fun _ ->
+        prerr_endline ("metasenv goals: " ^ String.concat " "
+          (List.map (fun (g, _, _) -> string_of_int g)
+            (MatitaScript.current ())#proofMetasenv));
+        prerr_endline ("stack: " ^ Continuationals.Stack.pp
+          (MatitaTypes.get_stack (MatitaScript.current ())#status)));
+(*     addDebugItem "ask record choice"
+      (fun _ ->
+        MatitaLog.debug (string_of_int
+          (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
+          ~fields:["a"; "b"; "c"]
+          ~records:[
+            ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
+            ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
+          ()))); *)
+    addDebugItem "rotate light bulbs"
+      (fun _ ->
+         let nb = gui#main#hintNotebook in
+         nb#goto_page ((nb#current_page + 1) mod 3));
+    addDebugItem "print runtime dir"
+      (fun _ ->
+        prerr_endline BuildTimeConf.runtime_base_dir);
+    addDebugItem "disable all (pretty printing) notations"
+      (fun _ -> CicNotation.set_active_notations []);
+    addDebugItem "enable all (pretty printing) notations"
+      (fun _ ->
+        CicNotation.set_active_notations
+          (List.map fst (CicNotation.get_all_notations ())));
+  end
+  (** Debugging }}} *)
+
+  (** {2 Command line parsing} *)
+
+let set_matita_mode () =
+  let matita_mode =
+    if Filename.basename Sys.argv.(0) = "cicbrowser"
+    then "cicbrowser"
+    else "matita"
+  in
+  Helm_registry.set "matita.mode" matita_mode
+
+  (** {2 Main} *)
 
-let _ = GtkThread.main ()
+let _ =
+  set_matita_mode ();
+  at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
+  Sys.catch_break true;
+  let args = Helm_registry.get_list Helm_registry.string "matita.args" in
+  if Helm_registry.get "matita.mode" = "cicbrowser" then  (* cicbrowser *)
+    let browser = MatitaMathView.cicBrowser () in
+    let uri = match args with [] -> "cic:/" | _ -> String.concat " " args in
+    browser#loadInput uri
+  else begin  (* matita *)
+    (try gui#loadScript (List.hd args) with Failure _ -> ());
+    gui#main#mainWin#show ();
+  end;
+  try
+    GtkThread.main ()
+  with Sys.Break -> ()
 
+(* vim:set foldmethod=marker: *)