snapshot, notably:

- attributes support
- new ApplyTransformation interface
- simil-coma commit, browser is partially implemented :(

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index 39efbf62b5864c58a91671e4b3404a6780d12feb..e75988386ba55cd0c8f3cd7326f93671d091faf2 100644 (file)
--- a/helm/matita/buildTimeConf.ml.in
+++ b/helm/matita/buildTimeConf.ml.in
@@ -29,5 +29,5 @@ let undo_history_size = 10;;
 let console_history_size = 100;;
 let gtkrc = "@MATITA_GTKRC@";;
 let base_uri = "cic:/matita";;
-let phrase_sep = ";;";;
+let phrase_sep = ".";;
 

diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample
index 6aee8a561c292d1d368f0ca0afb3da3d65269dc3..9035d2a78f944f55420ac0663dc578d4591505ac 100644 (file)
--- a/helm/matita/matita.conf.xml.sample
+++ b/helm/matita/matita.conf.xml.sample
@@ -1,8 +1,8 @@
 <?xml version="1.0" encoding="utf-8"?>
 <helm_registry>
   <section name="prefs">
-<!--     <key name="server">mowgli.cs.unibo.it</key> -->
-    <key name="server">localhost</key>
+    <key name="server">mowgli.cs.unibo.it</key>
+<!--     <key name="server">localhost</key> -->
   </section>
   <section name="matita">
     <key name="glade_file">matita.glade</key>

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 12b772a953306d6ce398c40808e13f0d7296de04..58c7132927342cce24a16c23bb3b31ee04d3b258 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -2262,6 +2262,8 @@ Copyright (C) 2004,
 </widget>
 
 <widget class="GtkWindow" id="BrowserWin">
+  <property name="width_request">400</property>
+  <property name="height_request">500</property>
   <property name="title" translatable="yes">Cic browser</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_NONE</property>
@@ -2457,36 +2459,25 @@ Copyright (C) 2004,
          </child>
 
          <child>
-           <widget class="GtkNotebook" id="BrowserNotebook">
+           <widget class="GtkFrame" id="frame1">
              <property name="visible">True</property>
-             <property name="can_focus">True</property>
-             <property name="show_tabs">True</property>
-             <property name="show_border">True</property>
-             <property name="tab_pos">GTK_POS_TOP</property>
-             <property name="scrollable">False</property>
-             <property name="enable_popup">False</property>
-
-             <child>
-               <placeholder/>
-             </child>
+             <property name="label_xalign">0</property>
+             <property name="label_yalign">0</property>
+             <property name="shadow_type">GTK_SHADOW_NONE</property>
 
              <child>
-               <widget class="GtkLabel" id="label9">
+               <widget class="GtkScrolledWindow" id="ScrolledBrowser">
                  <property name="visible">True</property>
-                 <property name="label" translatable="yes">current proof</property>
-                 <property name="use_underline">False</property>
-                 <property name="use_markup">False</property>
-                 <property name="justify">GTK_JUSTIFY_LEFT</property>
-                 <property name="wrap">False</property>
-                 <property name="selectable">False</property>
-                 <property name="xalign">0.5</property>
-                 <property name="yalign">0.5</property>
-                 <property name="xpad">0</property>
-                 <property name="ypad">0</property>
+                 <property name="can_focus">True</property>
+                 <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+                 <property name="shadow_type">GTK_SHADOW_NONE</property>
+                 <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+                 <child>
+                   <placeholder/>
+                 </child>
                </widget>
-               <packing>
-                 <property name="type">tab</property>
-               </packing>
              </child>
            </widget>
            <packing>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 107691932b6fc5b71eaa4226ab192087f3847de1..13ec23a6e57697495c06a50246fef6d072f2b42a 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -88,6 +88,7 @@ let _ = (* attach observers to proof status *)
   currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
 
 let mathViewer = MatitaMathView.mathViewer ()
+let cicBrowser = MatitaMathView.cicBrowser ()
 let interpreter =
   let console = (gui#console :> MatitaTypes.console) in
   let currentProof = (currentProof :> MatitaTypes.currentProof) in
@@ -213,7 +214,8 @@ let _ =
       let i = ref 0 in
       List.iter
         (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
-        sequent_viewer#get_selected_terms)
+        sequent_viewer#get_selected_terms);
+    addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ());
   end
 
   (** </DEBUGGING> *)

diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml
index 523e33ea2458d86cf249251c22eded2aa5d97992..c77ded6be1d2271d3dbf0bfd7738d878f2333620 100644 (file)
--- a/helm/matita/matitaCicMisc.ml
+++ b/helm/matita/matitaCicMisc.ml
@@ -27,11 +27,11 @@
 let cicCurrentProof (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [], [])
 
   (** create a Cic.Constant from a given proof *)
 let cicConstant (uri, metasenv, bo, ty) =
   let uri = MatitaTypes.unopt_uri uri in
     (* TODO CSC: Wrong: [] is just plainly wrong *)
-  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [])
+  Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], [])
 

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index e9db307d44f8a1ec41ce34fc2038709352181f18..689984774b7369816c5f9ced0825d143b049a5b3 100644 (file)
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -841,14 +841,14 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMisc.image (GtkMisc.Image.cast
         (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata))
     method image187 = image187
-    val browserNotebook =
-      new GPack.notebook (GtkPack.Notebook.cast
-        (Glade.get_widget_msg ~name:"BrowserNotebook" ~info:"GtkNotebook" xmldata))
-    method browserNotebook = browserNotebook
-    val label9 =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"label9" ~info:"GtkLabel" xmldata))
-    method label9 = label9
+    val frame1 =
+      new GBin.frame (GtkBin.Frame.cast
+        (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
+    method frame1 = frame1
+    val scrolledBrowser =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledBrowser = scrolledBrowser
     method reparent parent =
       browserWinEventBox#misc#reparent parent;
       toplevel#destroy ()

diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli
index 113538361a591607cddf00b875adf3ef829a467f..a84c1328af3d27800718c5df68a2d6663be09d9c 100644 (file)
--- a/helm/matita/matitaGeneratedGui.mli
+++ b/helm/matita/matitaGeneratedGui.mli
@@ -487,9 +487,9 @@ class browserWin :
     val browserBackButton : GButton.button
     val browserForwardButton : GButton.button
     val browserHomeButton : GButton.button
-    val browserNotebook : GPack.notebook
     val browserWin : GWindow.window
     val browserWinEventBox : GBin.event_box
+    val frame1 : GBin.frame
     val hbox6 : GPack.box
     val hbox7 : GPack.box
     val image187 : GMisc.image
@@ -497,7 +497,7 @@ class browserWin :
     val image189 : GMisc.image
     val image190 : GMisc.image
     val label10 : GMisc.label
-    val label9 : GMisc.label
+    val scrolledBrowser : GBin.scrolled_window
     val toplevel : GWindow.window
     val vbox7 : GPack.box
     val xml : Glade.glade_xml Gtk.obj
@@ -506,10 +506,10 @@ class browserWin :
     method browserBackButton : GButton.button
     method browserForwardButton : GButton.button
     method browserHomeButton : GButton.button
-    method browserNotebook : GPack.notebook
     method browserWin : GWindow.window
     method browserWinEventBox : GBin.event_box
     method check_widgets : unit -> unit
+    method frame1 : GBin.frame
     method hbox6 : GPack.box
     method hbox7 : GPack.box
     method image187 : GMisc.image
@@ -517,8 +517,8 @@ class browserWin :
     method image189 : GMisc.image
     method image190 : GMisc.image
     method label10 : GMisc.label
-    method label9 : GMisc.label
     method reparent : GObj.widget -> unit
+    method scrolledBrowser : GBin.scrolled_window
     method toplevel : GWindow.window
     method vbox7 : GPack.box
     method xml : Glade.glade_xml Gtk.obj

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f8f252b524f3e3e697b6ae12f339bde0cbb1bd54..de5240e447ccacbf533609fe91f6b59f44e49f09 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -123,6 +123,7 @@ class gui file =
 *)
 
     method about = about
+    method browser = browser
     method check = check
     method console = console
     method fileSel = fileSel

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index 39657c58723cb6e091fbb2497b3033656ab0a521..419dc77eb52b7c3c7f96bfe2e419a976b6374d9e 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -34,6 +34,7 @@ class gui :
       (** {2 Access to lower-level GTK widgets} *)
 
     method about :        MatitaGeneratedGui.aboutWin
+    method browser :      MatitaGeneratedGui.browserWin
     method check :        MatitaGeneratedGui.checkWin
     method fileSel :      MatitaGeneratedGui.fileSelectionWin
     method main :         MatitaGeneratedGui.mainWin

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index bb43d67e0ae950159bb249a45d09262cb46bbaff..b891f4e9457c2d059d710445dbc61ee03a42e270 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -54,8 +54,8 @@ let qualify name =
   else
     String.concat "/" [baseuri; name]
 let split_obj = function
-  | Cic.Constant (name, body, ty, _)
-  | Cic.Variable (name, body, ty, _) -> (name, body, ty)
+  | Cic.Constant (name, body, ty, _, attrs)
+  | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
   | _ -> assert false
 
 let canonical_context metano metasenv =
@@ -260,9 +260,9 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
     * - save object to disk in xml format
     * - register uri to the getter 
     * - save universe file *)
-let add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph () =
+let add_constant_to_world ~dbd ~uri ?body ~ty ?(attrs = []) ~ugraph () =
   let name = UriManager.name_of_uri uri in
-  let obj = Cic.Constant (name, body, ty, []) in
+  let obj = Cic.Constant (name, body, ty, [], attrs) in
   let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
   CicEnvironment.add_type_checked_term uri (obj, ugraph);
   MetadataDb.index_constant ~dbd
@@ -316,7 +316,7 @@ class commandState
           let (uri, (indTypes, params, leftno)) =
             inddef_of_ast params indTypes disambiguator
           in
-          let obj = Cic.InductiveDefinition (indTypes, params, leftno) in
+          let obj = Cic.InductiveDefinition (indTypes, params, leftno, []) in
           let ugraph =
             CicTypeChecker.typecheck_mutual_inductive_defs uri
               (indTypes, params, leftno) CicUniv.empty_ugraph
@@ -325,20 +325,21 @@ class commandState
           CicEnvironment.put_inductive_definition uri (obj, ugraph);
           MetadataDb.index_inductive_def ~dbd
             ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
-          let msgs = ref [] in
           let elim sort =
             try
               let obj = CicElim.elim_of ~sort uri 0 in
-              let (name, body, ty) = split_obj obj in
-              let uri = UriManager.uri_of_string (qualify name ^ ".con") in
+              let (name, body, ty, attrs) = split_obj obj in
+              let suri = qualify name ^ ".con" in
+              let uri = UriManager.uri_of_string suri in
                 (* TODO Zack: make CicElim returns a universe *)
               let ugraph = CicUniv.empty_ugraph in
-              add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph ();
-              msgs := (sprintf "%s defined" name) :: !msgs;
+              add_constant_to_world ~dbd ~uri ?body ~ty ~attrs ~ugraph ();
+              console#echo_message
+                (sprintf "%s eliminator (automatically) defined" suri)
             with CicElim.Can_t_eliminate -> ()
           in
           List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
-          Echo (String.concat "\n" (List.rev !msgs))
+          Quiet
       | TacticAst.Command TacticAst.Quit ->
           currentProof#quit ();
           New_state Command (* dummy answer, useless *)
@@ -441,6 +442,7 @@ class proofState
           let proof = currentProof#proof in
           let (uri, metasenv, bo, ty) = proof#proof in
           let uri = MatitaTypes.unopt_uri uri in
+          let suri = UriManager.string_of_uri uri in
             (* TODO Zack this function probably should not simply fail with
             * Failure, but rather raise some more meaningful exception *)
           if metasenv <> [] then failwith "Proof not completed";
@@ -454,6 +456,7 @@ class proofState
           add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph ();
           currentProof#abort ();
           (match mathViewer with None -> () | Some v -> v#unload ());
+          console#echo_message (sprintf "%s defined" suri);
           New_state Command
       | TacticAst.Seq tacticals ->
           (* TODO Zack check for proof completed at each step? *)

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f264ec413cad9c51932a3c804d3c88fe3ca60c9c..03803c2b94073eb3e5a72517fcda403e6b36516e 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -85,8 +85,17 @@ class clickable_math_view obj =
       | None   -> self#set_selection None
   end
 
+let clickable_math_view =
+  GtkBase.Widget.size_params
+    ~cont:(OgtkMathViewProps.pack_return (fun p ->
+      OgtkMathViewProps.set_params
+        (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p))
+        ~font_size:None ~log_verbosity:None))
+    []
+let clickable_math_view () = clickable_math_view ()
+
 class proof_viewer obj =
-  object(self)
+  object (self)
 
     inherit clickable_math_view obj
 
@@ -94,16 +103,14 @@ class proof_viewer obj =
     val mutable current_mathml = None
 
     method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
-      let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
-          ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
-        Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+      let uri = unopt_uri uri_opt in
+      let obj = cicCurrentProof proof in
+      let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+           ids_to_hypotheses)) =
+        ApplyTransformation.mml_of_cic_object uri obj
       in
       current_infos <- Some (ids_to_terms, ids_to_father_ids,
         ids_to_conjectures, ids_to_hypotheses);
-      let mathml =
-        ApplyTransformation.mml_of_cic_object ~explode_all:true
-          (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
-      in
       debug_print "load_proof: dumping MathML to ./proof";
       ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
       match current_mathml with
@@ -269,6 +276,18 @@ let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
         ~font_size ~log_verbosity))
     []
 
+class cicBrowser =
+  object (self)
+    val widget =
+      let gui = MatitaGui.instance () in
+      sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add ()
+
+    initializer
+      widget#set_href_callback (Some (fun uri -> self#load_uri uri))
+
+    method load_uri uri = ()
+  end
+
 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
@@ -284,11 +303,6 @@ let proof_viewer_instance =
   ) in
   fun () -> Lazy.force instance
 
-let sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ~set_goal ()
-=
-  new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
-
 class mathViewer =
   let href_callback: (UriManager.uri -> unit) option ref = ref None in
   object
@@ -314,5 +328,12 @@ class mathViewer =
     method unload () = (proof_viewer_instance ())#unload
   end
 
+let sequents_viewer ~(notebook:GPack.notebook)
+  ~(sequent_viewer:sequent_viewer) ~set_goal ()
+=
+  new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
+
 let mathViewer () = new mathViewer
 
+let cicBrowser () = new cicBrowser
+

diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli
index 04d96befeb8cc0a16cb1cbf79be51ba4c2c4c1fd..8b5ca89acd1ced41d4f1aacf172244044021c260 100644 (file)
--- a/helm/matita/matitaMathView.mli
+++ b/helm/matita/matitaMathView.mli
@@ -64,6 +64,13 @@ class type sequents_viewer =
     method goto_sequent: int -> unit  (* to be called _after_ load_sequents *)
   end
 
+class type cicBrowser =
+  object
+    method load_uri: UriManager.uri -> unit
+  end
+
+(** {2 Constructors} *)
+
 val proof_viewer:
   ?hadjustment:GData.adjustment ->
   ?vadjustment:GData.adjustment ->
@@ -76,10 +83,6 @@ val proof_viewer:
   unit ->
     proof_viewer
 
-  (** singleton proof_viewer instance.
-  * Uses singleton GUI instance *)
-val proof_viewer_instance: unit -> proof_viewer
-
 val sequent_viewer:
   ?hadjustment:GData.adjustment ->
   ?vadjustment:GData.adjustment ->
@@ -99,5 +102,13 @@ val sequents_viewer:
   unit ->
     sequents_viewer
 
+val cicBrowser: unit -> cicBrowser
+
 val mathViewer: unit -> MatitaTypes.mathViewer
 
+(** {2 Singletons} *)
+
+  (** singleton proof_viewer instance.
+  * Uses singleton GUI instance *)
+val proof_viewer_instance: unit -> proof_viewer
+

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 64870249019b5e8e79ef29f062870bf5504d4584..3f394cdb1108e9dc70158ad99d51c66b714bccc0 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -84,7 +84,7 @@ let interpreter =
     ~disambiguator ~currentProof ~console ~dbd ()
 
 let run_script fname =
-  message (sprintf "execution of %s started." fname);
+  message (sprintf "execution of %s started:" fname);
   let script =
     let ic = open_in fname in
     let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in
@@ -92,7 +92,7 @@ let run_script fname =
     ast
   in
   let rec aux = function
-    | [] -> ()
+    | [] -> ()  (* script is over *)
     | DisambiguateTypes.Comment _ :: tl -> aux tl
     | DisambiguateTypes.Command ast :: tl ->
         let loc =
@@ -107,7 +107,8 @@ let run_script fname =
         else
           aux tl
   in
-  aux script
+  aux script;
+  message (sprintf "execution of %s completed." fname)
 
 let _ = List.iter run_script scripts