X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=6308eab86e3035f0fe170ce0b24bbf82f21cb843;hb=41be5e85a1103a5b14495bb487995a6a88e79c48;hp=dc3fb07cec55ee46627996d934cee317bd8bfd40;hpb=215cb34e905e846d37c873224df1ec30bf81ba87;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index dc3fb07ce..6308eab86 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -29,6 +29,8 @@ open MatitaGeneratedGui
 open MatitaGtkMisc
 open MatitaMisc
 
+exception Found of int
+
 let gui_instance = ref None
 
 class type browserWin =
@@ -51,7 +53,7 @@ class console ~(buffer: GText.buffer) () =
     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
     method clear () =
       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
-    method log_callback (tag: MatitaLog.log_tag) s =
+    method log_callback (tag: HLog.log_tag) s =
       match tag with
       | `Debug -> self#debug (s ^ "\n")
       | `Error -> self#error (s ^ "\n")
@@ -61,27 +63,30 @@ class console ~(buffer: GText.buffer) () =
         
 let clean_current_baseuri status = 
     try  
-      let baseuri = MatitaTypes.get_string_option status "baseuri" in
-      MatitacleanLib.clean_baseuris [baseuri]
-    with MatitaTypes.Option_error _ -> ()
+      let baseuri = GrafiteTypes.get_string_option status "baseuri" in
+      let basedir = Helm_registry.get "matita.basedir" in
+      LibraryClean.clean_baseuris ~basedir [baseuri]
+    with GrafiteTypes.Option_error _ -> ()
 
 let ask_and_save_moo_if_needed parent fname status = 
+  let basedir = Helm_registry.get "matita.basedir" in
+  let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in
+  let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
   let save () =
-    let moo_fname = MatitacleanLib.obj_file_of_script fname in
-    MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
+    let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+    GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
+    LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+  in
   if (MatitaScript.current ())#eos &&
-     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+     status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then
     begin
-      let mooname = 
-        MatitacleanLib.obj_file_of_script fname
-      in
       let rc = 
         MatitaGtkMisc.ask_confirmation
         ~title:"A .moo can be generated"
         ~message:(Printf.sprintf 
           "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          (Filename.basename mooname) (Filename.basename fname))
+          (Filename.basename moo_fname) (Filename.basename fname))
         ~parent ()
       in
       let b = 
@@ -91,7 +96,7 @@ let ask_and_save_moo_if_needed parent fname status =
         | `CANCEL -> raise MatitaTypes.Cancel 
       in
       if b then
-        save ()
+          save ()
       else
         clean_current_baseuri status
     end
@@ -437,7 +442,6 @@ class gui () =
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
         (fun _ -> develList#toplevel#misc#hide();true));
-      let selected_devel = ref None in
       connect_menu_item main#developmentsMenuItem
         (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
       
@@ -470,7 +474,7 @@ class gui () =
               newDevel#toplevel#misc#hide()
             end
           else
-            MatitaLog.error ("The selected root does not contain " ^ 
+            HLog.error ("The selected root does not contain " ^ 
               match next_devel_must_contain with 
               | Some x -> x 
               | _ -> assert false));
@@ -568,18 +572,46 @@ class gui () =
         ~check:main#fullscreenMenuItem;
       main#fullscreenMenuItem#set_active false;
         (* log *)
-      MatitaLog.set_log_callback self#console#log_callback;
+      HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
         (fun exn ->
           if not (Helm_registry.get_bool "matita.debug") then
-            MatitaLog.error (MatitaExcPp.to_string exn)
+           let floc, msg = MatitaExcPp.to_string exn in
+            begin
+             match floc with
+                None -> ()
+              | Some floc ->
+                 let (x, y) = HExtlib.loc_of_floc floc in
+                 let script = MatitaScript.current () in
+                 let locked_mark = script#locked_mark in
+                 let error_tag = script#error_tag in
+                 let baseoffset =
+                  (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+                 let x' = baseoffset + x in
+                 let y' = baseoffset + y in
+                 let x_iter = source_buffer#get_iter (`OFFSET x') in
+                 let y_iter = source_buffer#get_iter (`OFFSET y') in
+                 source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+                 let id = ref None in
+                 id := Some (source_buffer#connect#changed ~callback:(fun () ->
+                   source_buffer#remove_tag error_tag
+                     ~start:source_buffer#start_iter
+                     ~stop:source_buffer#end_iter;
+                   match !id with
+                   | None -> assert false (* a race condition occurred *)
+                   | Some id ->
+                       (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
+                 source_buffer#place_cursor
+                  (source_buffer#get_iter (`OFFSET x'));
+            end;
+            HLog.error msg
           else raise exn);
         (* script *)
-      let _ = source_buffer#connect#changed (fun _ -> next_ligatures <- []) in
+      ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
-            MatitaLog.warn (sprintf "can't load language file %s"
+            HLog.warn (sprintf "can't load language file %s"
               BuildTimeConf.lang_file)
         | Some matita_lang ->
             source_buffer#set_language matita_lang;
@@ -621,7 +653,6 @@ class gui () =
       in
       let loadScript () =
         let script = s () in 
-        let status = script#status in
         try 
           match self#chooseFile () with
           | Some f -> 
@@ -700,25 +731,16 @@ class gui () =
       connect_button main#scriptRetractButton retract;
       connect_button main#scriptTopButton top;
       connect_button main#scriptBottomButton bottom;
-      connect_key GdkKeysyms._Down advance;
-      connect_key GdkKeysyms._Up retract;
-      connect_key GdkKeysyms._Home top;
-      connect_key GdkKeysyms._End bottom;
       connect_button main#scriptJumpButton jump;
+      connect_menu_item main#scriptAdvanceMenuItem advance;
+      connect_menu_item main#scriptRetractMenuItem retract;
+      connect_menu_item main#scriptTopMenuItem top;
+      connect_menu_item main#scriptBottomMenuItem bottom;
+      connect_menu_item main#scriptJumpMenuItem jump;
       connect_menu_item main#openMenuItem   loadScript;
       connect_menu_item main#saveMenuItem   saveScript;
       connect_menu_item main#saveAsMenuItem saveAsScript;
       connect_menu_item main#newMenuItem    newScript;
-      connect_key GdkKeysyms._period
-        (fun () ->
-          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
-            ".\n";
-          advance ());
-      connect_key GdkKeysyms._Return
-        (fun () ->
-          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
-            "\n";
-          advance ());
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)
@@ -786,15 +808,43 @@ class gui () =
         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
+      let get_ligature word =
+        let len = String.length word in
+        let aux_tex () =
+          try
+            for i = len - 1 downto 0 do
+              if HExtlib.is_alpha word.[i] then ()
+              else
+                (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
+            done;
+            None
+          with Found i ->
+            if i = ~-1 then None else Some (String.sub word i (len - i))
+        in
+        let aux_ligature () =
+          try
+            for i = len - 1 downto 0 do
+              if CicNotationLexer.is_ligature_char word.[i] then ()
+              else raise (Found (i+1))
+            done;
+            raise (Found 0)
+          with
+          | Found i ->
+              (try
+                Some (String.sub word i (len - i))
+              with Invalid_argument _ -> None)
+        in
+        match aux_tex () with
+        | Some macro -> macro
+        | None -> (match aux_ligature () with Some l -> l | None -> word)
+      in
       (match next_ligatures with
       | [] -> (* find ligatures and fill next_ligatures, then try again *)
-          let last_word = iter#get_slice ~stop:iter#copy#backward_word_start in
-          let len = String.length last_word in
-          let i = ref (len - 1) in
-          while !i >= 0 && CicNotationLexer.is_ligature_char last_word.[!i] do
-            decr i
-          done;
-          let ligature = String.sub last_word (!i + 1) (len - (!i + 1)) in
+          let last_word =
+            iter#get_slice
+              ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
+          in
+          let ligature = get_ligature last_word in
           (match CicNotationLexer.lookup_ligatures ligature with
           | [] -> ()
           | hd :: tl ->
@@ -1030,7 +1080,6 @@ let interactive_uri_choice
       (selection_mode :> Gtk.Tags.selection_mode);
     let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
-    let nonvars = ref false in
     (match copy_cb with
     | None -> ()
     | Some cb ->
@@ -1126,7 +1175,6 @@ let interactive_interp_choice () choices =
   assert (choices <> []);
   let dialog = gui#newRecordDialog () in
   let model = new interpModel dialog#recordChoiceTreeView choices in
-  let interp_len = List.length (List.hd choices) in
   dialog#recordChoiceDialog#set_title "Interpretation choice";
   dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
   let interp_no = ref None in