- LexiconAst merged into GrafiteAst

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 9271384c1df9ec33e4db9327cda648c7e3052b9b..a42500bd6bf16fd524efa2906d38f5cb18dd4a5f 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -72,23 +72,10 @@ let clean_current_baseuri grafite_status =
 let save_moo grafite_status = 
   let script = MatitaScript.current () in
   let baseuri = grafite_status#baseuri in
-  let no_pstatus = 
-    grafite_status#proof_status = GrafiteTypes.No_proof 
-  in
-  match script#bos, script#eos, no_pstatus with
-  | true, _, _ -> ()
-  | _, true, true ->
-     let moo_fname = 
-       LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
-        ~writable:true in
-     let lexicon_fname =
-       LibraryMisc.lexicon_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true
-     in
-     GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
-     LexiconMarshal.save_lexicon lexicon_fname
-      grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
-     NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+  match script#bos, script#eos with
+  | true, _ -> ()
+  | _, true ->
+     GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
       grafite_status#dump
   | _ -> clean_current_baseuri grafite_status 
 ;;
@@ -333,13 +320,13 @@ let rec interactive_error_interp ~all_passes
                   let alias =
                    match k with
                    | DisambiguateTypes.Id id ->
-                       LexiconAst.Ident_alias (id, desc)
+                       GrafiteAst.Ident_alias (id, desc)
                    | DisambiguateTypes.Symbol (symb, i)-> 
-                       LexiconAst.Symbol_alias (symb, i, desc)
+                       GrafiteAst.Symbol_alias (symb, i, desc)
                    | DisambiguateTypes.Num i ->
-                       LexiconAst.Number_alias (i, desc)
+                       GrafiteAst.Number_alias (i, desc)
                   in
-                   LexiconAstPp.pp_alias alias)
+                   GrafiteAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert
@@ -863,14 +850,16 @@ class gui () =
           | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
-        ~callback:(function
-          | true ->
-              CicNotation.set_active_notations
-                (List.map fst (CicNotation.get_all_notations ()))
-          | false ->
-              CicNotation.set_active_notations []);
+        ~callback:(function b ->
+          let s = s () in
+          let status =
+           Interpretations.toggle_active_interpretations s#grafite_status b
+          in
+           assert false (* MATITA1.0 ???
+           s#set_grafite_status status*)
+         );
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
-        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+        ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
@@ -887,18 +876,8 @@ class gui () =
           else raise exn);
         (* script *)
       let _ =
-        let source_language_manager =
-         GSourceView2.source_language_manager ~default:true in
-        source_language_manager#set_search_path
-         (BuildTimeConf.runtime_base_dir ::
-           source_language_manager#search_path);
-        match source_language_manager#language "grafite" with
-        | None ->
-            HLog.warn(sprintf "can't load a language file for \"grafite\" in %s"
-              BuildTimeConf.runtime_base_dir)
-        | Some x as matita_lang ->
-            source_buffer#set_language matita_lang;
-            source_buffer#set_highlight_syntax true
+       source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
+       source_buffer#set_highlight_syntax true
       in
       let disableSave () =
         (s())#assignFileName None;
@@ -1008,8 +987,6 @@ class gui () =
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
           c#load (`About `Hints));
-      connect_menu_item main#showAutoGuiMenuItem 
-        (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
       connect_menu_item main#showTermGrammarMenuItem 
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
@@ -1379,8 +1356,7 @@ class gui () =
 
     method private updateFontSize () =
       self#sourceView#misc#modify_font_by_name
-        (sprintf "%s %d" BuildTimeConf.script_font font_size);
-      MatitaAutoGui.set_font_size font_size
+        (sprintf "%s %d" BuildTimeConf.script_font font_size)
 
     method increaseFontSize () =
       font_size <- font_size + 1;
@@ -1415,11 +1391,10 @@ let interactive_uri_choice
   ~id uris
 =
   let gui = instance () in
-  let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
   if (selection_mode <> `SINGLE) &&
     (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
   then
-    Lazy.force nonvars_uris
+    uris
   else begin
     let dialog = gui#newUriDialog () in
     if hide_uri_entry then
@@ -1445,7 +1420,7 @@ let interactive_uri_choice
           | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
-    List.iter model#easy_append (List.map UriManager.string_of_uri uris);
+    List.iter model#easy_append (List.map NReference.string_of_reference uris);
     dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
     let return v =
       choices := v;
@@ -1454,20 +1429,20 @@ let interactive_uri_choice
     in
     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
     connect_button dialog#uriChoiceConstantsButton (fun _ ->
-      return (Some (Lazy.force nonvars_uris)));
+      return (Some uris));
     if ok_action = `AUTO then
       connect_button dialog#uriChoiceAutoButton (fun _ ->
         Helm_registry.set_bool "matita.auto_disambiguation" true;
-        return (Some (Lazy.force nonvars_uris)))
+        return (Some uris))
     else
       connect_button dialog#uriChoiceAutoButton (fun _ ->
         match model#easy_selection () with
         | [] -> ()
-        | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+        | uris -> return (Some (List.map NReference.reference_of_string uris)));
     connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()
-      | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+      | uris -> return (Some (List.map NReference.reference_of_string uris)));
     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
     dialog#uriChoiceDialog#show ();
     GtkThread.main ();