snapshot

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index e7f4f677b5dc06f8ef56de8ccbd3bf8d0e9ae5b5..a9ea5d40c201138a240bf900833c92ebb0c2d04e 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -7,7 +7,7 @@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
 
 OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O)
 OCAML_THREADS_FLAGS = -thread
-OCAML_DEBUG_FLAGS =
+OCAML_DEBUG_FLAGS = -g
 OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS)
 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 6420b2aa514ad4e4cd7e1d44d752146d84cbf93b..103e27673fe8ee2076b2b3908739e52f28ef81af 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -51,7 +51,7 @@
                          <property name="use_underline">True</property>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image174">
+                           <widget class="GtkImage" id="image182">
                              <property name="visible">True</property>
                              <property name="stock">gtk-new</property>
                              <property name="icon_size">1</property>
@@ -94,7 +94,7 @@
                          <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image175">
+                           <widget class="GtkImage" id="image183">
                              <property name="visible">True</property>
                              <property name="stock">gtk-open</property>
                              <property name="icon_size">1</property>
@@ -115,7 +115,7 @@
                          <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image176">
+                           <widget class="GtkImage" id="image184">
                              <property name="visible">True</property>
                              <property name="stock">gtk-save</property>
                              <property name="icon_size">1</property>
@@ -135,7 +135,7 @@
                          <property name="use_underline">True</property>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image177">
+                           <widget class="GtkImage" id="image185">
                              <property name="visible">True</property>
                              <property name="stock">gtk-save-as</property>
                              <property name="icon_size">1</property>
@@ -162,7 +162,7 @@
                          <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                          <child internal-child="image">
-                           <widget class="GtkImage" id="image178">
+                           <widget class="GtkImage" id="image186">
                              <property name="visible">True</property>
                              <property name="stock">gtk-quit</property>
                              <property name="icon_size">1</property>
@@ -246,7 +246,7 @@
                          <property name="visible">True</property>
                          <property name="label" translatable="yes">Toggle console</property>
                          <property name="use_underline">True</property>
-                         <accelerator key="x" modifiers="GDK_MOD1_MASK" signal="activate"/>
+                         <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
                        </widget>
                      </child>
                    </widget>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 7c9502bd414cc89b674d00a1d216a77baf8b4610..49488a94dfe3fe38bb5d593933df741f7e6bfe93 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -232,6 +232,7 @@ let _ =
   (** </DEBUGGING> *)
 
 let _ =
+(*   CicEnvironment.set_trust (fun _ -> false); *)
   (try
     load_script Sys.argv.(1)
   with Invalid_argument _ -> ());

diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml
index 222055e6539a59b8b9ecfed8bf3434d746bcb936..889d8e2d80244eb0aa23062347f4875819a6c401 100644 (file)
--- a/helm/matita/matitaConsole.ml
+++ b/helm/matita/matitaConsole.ml
@@ -31,6 +31,7 @@ open MatitaTypes
 let default_prompt = ""
 let default_phrase_sep = "."
 let default_callback = fun (phrase: string) -> true
+let bullet = "∙"
 
 let message_props = [ `STYLE `ITALIC ]
 let error_props = [ `WEIGHT `BOLD ]
@@ -92,6 +93,7 @@ class console
     val history = new history BuildTimeConf.console_history_size
 
     val mutable handle_position = 450
+    val mutable last_phrase = ""
 
     initializer
       let buf = self#buffer in
@@ -107,13 +109,15 @@ class console
           (Pcre.pmatch ~rex:trailing_NL_RE text)
         then
           let inserted_text =
-            buf#get_text
-              ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
-              ~stop:buf#end_iter ()
+            MatitaMisc.strip_trailing_blanks
+              (buf#get_text
+                ~start:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
+                ~stop:buf#end_iter ())
           in
           let pat = (Pcre.quote _phrase_sep) ^ "\\s*$" in
           if Pcre.pmatch ~pat inserted_text then begin (* complete phrase *)
             self#lock;
+            last_phrase <- inserted_text;
             self#invoke_callback inserted_text;
             self#echo_prompt ()
           end));
@@ -141,15 +145,13 @@ class console
       buf#insert ~iter:buf#end_iter phrase
 
     method private invoke_callback phrase =
-      history#add (* do not push trailing phrase separator *)
-        (String.sub phrase 0
-          (String.length phrase - String.length _phrase_sep));
+      history#add phrase;
       if _callback phrase then begin
         self#hide ();
         self#clear ()
+      end
         (* else callback encountered troubles, don't hide console which
         probably contains error message *)
-      end
 
     method clear () =
       let buf = self#buffer in
@@ -221,6 +223,21 @@ class console
       | StatefulProofEngine.Tactic_failure exn ->
           self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn));
           false
+      | CicTextualParser2.Parse_error (floc, msg) ->
+          let buf = self#buffer in
+          let (x, y) = CicAst.loc_of_floc floc in
+          let red = buf#create_tag [`FOREGROUND "red"] in
+          let (start_error_pos, end_error_pos) =
+            buf#end_iter#backward_chars (String.length last_phrase - x),
+            buf#end_iter#backward_chars (String.length last_phrase - y)
+          in
+          if x - y = 0 then (* no region to highlight, let's add an hint about
+                            where the error occured *)
+            buf#insert ~iter:end_error_pos ~tags:[red] bullet
+          else  (* highlight the region where the error occured *)
+            buf#apply_tag red ~start:start_error_pos ~stop:end_error_pos;
+          self#echo_error (sprintf "at character %d-%d: %s" x y msg);
+          false
       | exn ->
           self#echo_error (sprintf "Uncaught exception: %s"
             (Printexc.to_string exn));
@@ -241,3 +258,4 @@ let console
   in
   new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view
 
+(* vim: set encoding=utf8: *)

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index 883cb634ee5a30fe6fc2d232bf6c1ebc999b6071..f21a1967be6b46125e69d72f77aba146a0a6de49 100644 (file)
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -36,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
     method newMenu = newMenu
-    val image174 =
+    val image182 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image174" ~info:"GtkImage" xmldata))
-    method image174 = image174
+        (Glade.get_widget_msg ~name:"image182" ~info:"GtkImage" xmldata))
+    method image182 = image182
     val newMenu_menu =
       new GMenu.menu (GtkMenu.Menu.cast
         (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
@@ -56,26 +56,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method openMenuItem = openMenuItem
-    val image175 =
+    val image183 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image175" ~info:"GtkImage" xmldata))
-    method image175 = image175
+        (Glade.get_widget_msg ~name:"image183" ~info:"GtkImage" xmldata))
+    method image183 = image183
     val saveMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveMenuItem = saveMenuItem
-    val image176 =
+    val image184 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image176" ~info:"GtkImage" xmldata))
-    method image176 = image176
+        (Glade.get_widget_msg ~name:"image184" ~info:"GtkImage" xmldata))
+    method image184 = image184
     val saveAsMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveAsMenuItem = saveAsMenuItem
-    val image177 =
+    val image185 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image177" ~info:"GtkImage" xmldata))
-    method image177 = image177
+        (Glade.get_widget_msg ~name:"image185" ~info:"GtkImage" xmldata))
+    method image185 = image185
     val separator1 =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
@@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method quitMenuItem = quitMenuItem
-    val image178 =
+    val image186 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image178" ~info:"GtkImage" xmldata))
-    method image178 = image178
+        (Glade.get_widget_msg ~name:"image186" ~info:"GtkImage" xmldata))
+    method image186 = image186
     val editMenu =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))

diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli
index 74b2adfd0f11e0e3e85933b3edd3d822434cef40..6572f1a6df690d6be8143ce1ae27ddb348df6242 100644 (file)
--- a/helm/matita/matitaGeneratedGui.mli
+++ b/helm/matita/matitaGeneratedGui.mli
@@ -16,11 +16,11 @@ class mainWin :
     val helpMenu_menu : GMenu.menu
     val hideConsoleButton : GButton.button
     val image169 : GMisc.image
-    val image174 : GMisc.image
-    val image175 : GMisc.image
-    val image176 : GMisc.image
-    val image177 : GMisc.image
-    val image178 : GMisc.image
+    val image182 : GMisc.image
+    val image183 : GMisc.image
+    val image184 : GMisc.image
+    val image185 : GMisc.image
+    val image186 : GMisc.image
     val mainMenuBar : GMenu.menu_shell
     val mainStatusBar : GMisc.statusbar
     val mainVPanes : GPack.paned
@@ -64,11 +64,11 @@ class mainWin :
     method helpMenu_menu : GMenu.menu
     method hideConsoleButton : GButton.button
     method image169 : GMisc.image
-    method image174 : GMisc.image
-    method image175 : GMisc.image
-    method image176 : GMisc.image
-    method image177 : GMisc.image
-    method image178 : GMisc.image
+    method image182 : GMisc.image
+    method image183 : GMisc.image
+    method image184 : GMisc.image
+    method image185 : GMisc.image
+    method image186 : GMisc.image
     method mainMenuBar : GMenu.menu_shell
     method mainStatusBar : GMisc.statusbar
     method mainVPanes : GPack.paned

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 26cf9df086cacdd54511d0ded7bb5dab02fa40b0..6687ca69d38a8e60efad2fdaf0ca1e6c8336540b 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -81,8 +81,9 @@ class gui file =
       List.iter (fun w -> w#check_widgets ())
         (let c w = (w :> <check_widgets: unit -> unit>) in
          [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]);
-        (* "global" key bindings *)
-      List.iter (fun (key, callback) -> self#addKeyBinding key callback)
+        (* key bindings *)
+      List.iter (* global key bindings *)
+        (fun (key, callback) -> self#addKeyBinding key callback)
         [ GdkKeysyms._F3,
             toggle_win ~check:main#showProofMenuItem proof#proofWin;
           GdkKeysyms._F4,
@@ -91,6 +92,7 @@ class gui file =
             toggle_win ~check:main#showScriptMenuItem script#scriptWin;
           GdkKeysyms._x, (fun () -> console#toggle ());
         ];
+      add_key_binding GdkKeysyms._Escape console#hide main#consoleEventBox;
         (* about win *)
       ignore (about#aboutWin#event#connect#delete (fun _ -> true));
       ignore (main#aboutMenuItem#connect#activate (fun _ ->

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index bb62f51c98d334818e64eb013b6300e0ca783e3e..8c38cfc0bdaac85941241c1431317fcd4ea0cdde 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -91,8 +91,8 @@ class proof_viewer obj =
       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 /tmp/proof";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ());
+    debug_print "load_proof: dumping MathML to ./proof";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
     match current_mathml with
     |  None ->
         self#load_root ~root:mathml#get_documentElement ;
@@ -165,8 +165,8 @@ class sequent_viewer obj =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-    debug_print "load_sequent: dumping MathML to /tmp/prova";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ());
+    debug_print "load_sequent: dumping MathML to ./prova";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -237,7 +237,6 @@ class sequents_viewer ~(notebook:GPack.notebook)
       sequent_viewer#load_sequent _metasenv goal;
       try
         List.assoc goal goal2win ();
-        debug_print "set_selection none";
         sequent_viewer#set_selection None
       with Not_found -> assert false
 

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 83bdeb36f6ea3fcd55f6e7effc7635d00fad9ee2..1a55795a5536666d5c0adc993bdb5d1bcc1d7a13 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -45,3 +45,7 @@ let append_phrase_sep s =
   else
     s
 
+let strip_trailing_blanks =
+  let rex = Pcre.regexp "\\s*$" in
+  fun s -> Pcre.replace ~rex s
+

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index f8e8ee40c0c98d533fb996c83f366d8c9c5fe622..7a9ac0fc6f13aea57b535197b2302a88ce9c3abd 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -38,3 +38,5 @@ val is_proof_object: string -> bool
   * it *)
 val append_phrase_sep: string -> string
 
+val strip_trailing_blanks: string -> string
+