X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=3fb42b47de3bdffde7381ee3dc458f66cf3f5bbf;hb=69789d216abc552d2538089fd62b53af6f75b8b8;hp=82cabae040aed329ff6979d40d220a0ff01d3474;hpb=0b360e3e0202f27b62f1d3804315b665aca1a15a;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 82cabae04..3fb42b47d 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -764,10 +764,17 @@ let edit_aliases () =
           let uri =
            match resolve_id v with
               None -> assert false
-            | Some uri -> uri
+            | Some (CicTextualParser0.Uri uri) -> uri
+            | Some (CicTextualParser0.Term _)
+            | Some CicTextualParser0.Implicit -> assert false
           in
-           "alias " ^ v ^ " " ^
-             (string_of_cic_textual_parser_uri uri)
+           "alias " ^
+            (match v with
+                CicTextualParser0.Id id -> id
+              | CicTextualParser0.Symbol (descr,_) ->
+                 (* CSC: To be implemented *)
+                 assert false
+            )^ " " ^ (string_of_cic_textual_parser_uri uri)
         ) dom))) ;
   window#show () ;
   GtkThread.main ();
@@ -787,7 +794,7 @@ let edit_aliases () =
      let rec aux n =
       try
        let n' = Str.search_forward regexpr inputtext n in
-        let id = Str.matched_group 2 inputtext in
+        let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
         let uri =
          MQueryMisc.cic_textual_parser_uri_of_string
           ("cic:" ^ (Str.matched_group 5 inputtext))
@@ -797,7 +804,10 @@ let edit_aliases () =
            dom,resolve_id
           else
            id::dom,
-            (function id' -> if id = id' then Some uri else resolve_id id')
+            (function id' ->
+              if id = id' then
+               Some (CicTextualParser0.Uri uri)
+              else resolve_id id')
       with
        Not_found -> TermEditor.empty_id_to_uris
      in
@@ -916,14 +926,17 @@ let
    let obj = CicEnvironment.get_obj uri in
     show_in_show_window_obj uri obj
   in
-   let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
-    if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
-     let uri =
-      (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
-     in 
-      show_in_show_window_uri (UriManager.uri_of_string uri)
-    else
-     ignore (mmlwidget#action_toggle n)
+   let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+    match n with
+       None -> ()
+     | Some n' ->
+        if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+         let uri =
+          (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+         in 
+          show_in_show_window_uri (UriManager.uri_of_string uri)
+        else
+         ignore (mmlwidget#action_toggle n')
    in
     let _ =
      mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
@@ -1077,8 +1090,18 @@ exception AmbiguousInput;;
 
 (* A WIDGET TO ENTER CIC TERMS *)
 
+module ChosenTermEditor  = TexTermEditor;;
+module ChosenTextualParser0 = TexCicTextualParser0;;
+(*
+module ChosenTermEditor = TermEditor;;
+module ChosenTextualParser0 = CicTextualParser0;;
+*)
+
 module Callbacks =
  struct
+  let get_metasenv () = !ChosenTextualParser0.metasenv
+  let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
+
   let output_html msg = output_html (outputhtml ()) msg;;
   let interactive_user_uri_choice =
    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
@@ -1089,9 +1112,7 @@ module Callbacks =
  end
 ;;
 
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-module TermEditor' = TermEditor.Make(Callbacks);;
+module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
 
 (* OTHER FUNCTIONS *)
 
@@ -1237,7 +1258,7 @@ let new_inductive () =
        GBin.scrolled_window ~border_width:5
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
-       TermEditor'.term_editor
+       TexTermEditor'.term_editor
         ~width:400 ~height:20 ~packing:scrolled_window#add 
         ~share_id_to_uris_with:inputt ()
         ~isnotempty_callback:
@@ -1348,7 +1369,7 @@ let new_inductive () =
        GBin.scrolled_window ~border_width:5
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
-       TermEditor'.term_editor
+       TexTermEditor'.term_editor
         ~width:400 ~height:20 ~packing:scrolled_window#add
         ~share_id_to_uris_with:inputt ()
         ~isnotempty_callback:
@@ -1492,7 +1513,7 @@ let new_proof () =
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  (* moved here to have visibility of the ok button *)
  let newinputt =
-  TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+  TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
    ~share_id_to_uris_with:inputt ()
    ~isnotempty_callback:
     (function b ->
@@ -2725,7 +2746,7 @@ class rendering_window output (notebook : notebook) =
   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
  in
  let insert_query_item =
-  factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+  factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y
    ~callback:insertQuery in
  (* hbugs menu *)
  let hbugs_menu = factory0#add_submenu "HBugs" in
@@ -2763,7 +2784,7 @@ class rendering_window output (notebook : notebook) =
   GBin.scrolled_window ~border_width:5
    ~packing:frame#add () in
  let inputt =
-  TermEditor'.term_editor
+  TexTermEditor'.term_editor
    ~width:400 ~height:100 ~packing:scrolled_window1#add ()
    ~isnotempty_callback:
     (function b ->