X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=225738d581b88baee3bce8118e3d75fcc2f74d4f;hb=fd372e069bbcaa96dc5b2eef04f341b28850d726;hp=1f18e76a6a3aebc46af710b19b85fda96acfd958;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 1f18e76a6..225738d58 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -39,6 +39,17 @@ let list_map_fail f =
   in
   aux
 
+let add_trailing_slash =
+  let rex = Pcre.regexp "/$" in
+  fun s ->
+    if Pcre.pmatch ~rex s then s
+    else s ^ "/"
+
+let strip_blanks =
+  let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in
+  fun s ->
+    (Pcre.extract ~rex s).(1)
+
 (** inherit from this class if you want to access current script *)
 class scriptAccessor =
 object (self)
@@ -281,7 +292,7 @@ let cicBrowsers = ref []
 class type cicBrowser =
 object
   method load: MatitaTypes.mathViewer_entry -> unit
-  method loadList: string list -> MatitaTypes.mathViewer_entry-> unit
+  (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *)
   method loadInput: string -> unit
 end
 
@@ -289,32 +300,91 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   ()
 =
   let term_RE = Pcre.regexp "^term:(.*)" in
+  let whelp_RE = Pcre.regexp "^\\s*whelp" in
+  let uri_RE =
+    Pcre.regexp
+      "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$"
+  in
+  let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in
+  let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
   let trailing_slash_RE = Pcre.regexp "/$" in
+  let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
+  let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
+  let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
+  let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
   let gui = MatitaGui.instance () in
   let win = gui#newBrowserWin () in
+  let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
+  let combo,_ = GEdit.combo_box_text ~strings:queries () in
+  let activate_combo_query input q =
+    let q' = String.lowercase q in
+    let rec aux i = function
+      | [] -> failwith ("Whelp query '" ^ q ^ "' not found")
+      | h::_ when String.lowercase h = q' -> i
+      | _::tl -> aux (i+1) tl
+    in
+    combo#set_active (aux 0 queries);
+    win#queryInputText#set_text input
+  in
+  let set_whelp_query txt =
+    let query, arg = 
+      try
+        let q = Pcre.extract ~rex:whelp_query_RE txt in
+        q.(1), q.(2)
+      with Invalid_argument _ -> failwith "Malformed Whelp query"
+    in
+    activate_combo_query arg query
+  in
   let toplevel = win#toplevel in
   let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
   let fail msg =
     ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
       ~title:"Cic browser" ~msg ~cancel:false ());
   in
+  let tags =
+    [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
+      "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
+  in
   let handle_error f =
     try
       f ()
     with exn ->
       fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
   in
-  let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
+  let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
     inherit scriptAccessor
+    
+    (* Whelp bar queries *)
 
     initializer
+      activate_combo_query "" "locate";
+      win#comboVbox#add (combo :> GObj.widget);
+      let start_query () = 
+        let query = String.lowercase (List.nth queries combo#active) in
+        let input = win#queryInputText#text in
+        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
+        (MatitaScript.instance ())#advance ~statement ()
+      in
+      ignore(win#queryInputText#connect#activate ~callback:start_query);
+      ignore(combo#connect#changed ~callback:start_query);
+      win#whelpImage2#set_file "icons/whelp.png";
+      win#whelpBarToggleButton#set_active false;   
+      win#whelpBarBox#misc#hide ();
+      win#mathOrListNotebook#set_show_tabs false;
+      MatitaGtkMisc.connect_toggle_button win#whelpBarToggleButton 
+        (fun () -> 
+          if win#whelpBarToggleButton#active then
+            win#whelpBarBox#misc#show ()
+          else
+            win#whelpBarBox#misc#hide ());
+
       win#browserForwardButton#misc#set_sensitive false;
       win#browserBackButton#misc#set_sensitive false;
-      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
-        self#loadInput win#browserUri#text)));
+      ignore (win#browserUri#entry#connect#activate (handle_error' (fun () ->
+        self#loadInput win#browserUri#entry#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
-        self#_load (`About `Current_proof))));
+        self#load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
         (handle_error' self#refresh));
       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
@@ -329,11 +399,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           GMain.quit ();
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
-        ~callback:(fun _ _ ->
-          let old = win#browserUri#text in
-          self#loadInput (old ^ self#_getWhelpResultTreeviewSelection ())));
+        ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ())));
       mathView#set_href_callback (Some (fun uri ->
-        handle_error (fun () -> self#_load (`Uri uri))));
+        handle_error (fun () -> self#load (`Uri uri))));
       self#_load (`About `Blank);
       toplevel#show ()
 
@@ -341,19 +409,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     val mutable current_infos = None
     val mutable current_mathml = None
 
-    val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview
+    val model =
+      new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
 
-    method private _getWhelpResultTreeviewSelection () =
+    method private _getSelectedUri () =
       match model#easy_selection () with
-          | [u] -> u
-          | _ -> assert false
+      | [sel] when is_uri sel -> sel  (* absolute URI selected *)
+      | [sel] -> win#browserUri#entry#text ^ sel  (* relative URI selected *)
+      | _ -> assert false
 
     (** history RATIONALE 
      *
-     * all operations about history are done using _historyFoo
-     *
-     * only toplevel function like load loadList loadInput can call
-     * _historyAdd
+     * All operations about history are done using _historyFoo.
+     * Only toplevel functions (ATM load and loadInput) call _historyAdd.
      *)
           
     method private _historyAdd item = 
@@ -380,8 +448,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _showList = win#mathOrListNotebook#goto_page 1
     method private _showMath = win#mathOrListNotebook#goto_page 0
     
-
-    
     method private back () =
       try
         self#_load (self#_historyPrev ())
@@ -405,7 +471,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
             | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
             | `Dir dir -> self#_loadDir dir
             | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
-            | `Whelp (query, results) -> self#loadList results entry);
+            | `Whelp (query, results) -> 
+                set_whelp_query query;
+                self#_loadList (List.map (fun r -> "obj", r) results));
             self#setEntry entry
           end
       with
@@ -414,10 +482,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           fail (sprintf "object not found: %s" (UriManager.string_of_uri uri))
       | Browser_failure msg -> fail msg
 
-
     method private blank () =
-      mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement;
-      self#_showMath
+      self#_showMath;
+      mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
 
     method private _loadCheck term =
       failwith "not implemented _loadCheck";
@@ -445,16 +512,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       
     method private _loadDir dir = 
       let content = Http_getter.ls dir in
-      let l = List.map (function 
-        | Http_getter_types.Ls_section sec -> sec            
-        | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri
-        ) content
+      let l =
+        List.map
+          (function 
+            | Http_getter_types.Ls_section s -> "dir", s
+            | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri)
+          content
       in
+      if l = [] then raise (Browser_failure "no such directory");
       self#_loadList l
 
     method private setEntry entry =
-        win#browserUri#set_text (string_of_entry entry);
-        current_entry <- entry
+      win#browserUri#entry#set_text (string_of_entry entry);
+      current_entry <- entry
 
     method private _loadObj obj =
       self#_showMath; 
@@ -486,40 +556,39 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private _loadList l =
       model#list_store#clear ();
-      List.iter model#easy_append l;
+      List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
       self#_showList
     
-    (** { public methods } *)
+    (** { public methods, all must call _load!! } *)
       
-    method load uri =
-      handle_error (fun () -> self#_load uri);
-      self#_historyAdd uri
-
-    method loadList l entry = 
-      self#_loadList l;
-      self#_historyAdd entry
-    
-    method loadInput txt = 
-      let add_terminating_slash s =
-        if s.[String.length s - 1] <> '/' then s^"/" else s
+    method load entry =
+      handle_error (fun () -> self#_load entry; self#_historyAdd entry)
+
+    (**  this is what the browser does when you enter a string an hit enter *)
+    method loadInput txt =
+      let txt = strip_blanks txt in
+      let fix_uri txt =
+        UriManager.string_of_uri
+          (UriManager.strip_xpointer (UriManager.uri_of_string txt))
       in
-      let is_uri = 
-        try 
-          ignore(Http_getter.resolve txt); true
-        with
-        | Http_getter_types.Key_not_found _ 
-        | Http_getter_types.Unresolvable_URI _ -> false
-      in
-      let entry = 
-        if is_uri then
-          (`Uri txt)
-        else
-          (`Dir (add_terminating_slash txt))
-      in
-      self#_load entry;
-      self#_historyAdd entry
-      
-        
+      if is_whelp txt then begin
+        set_whelp_query txt;  
+        (MatitaScript.instance ())#advance ~statement:(txt ^ ".") ()
+      end else begin
+        let entry =
+          match txt with
+          | txt when is_uri txt -> `Uri (fix_uri txt)
+          | txt when is_dir txt -> `Dir (add_trailing_slash txt)
+          | txt ->
+              (try
+                entry_of_string txt
+              with Invalid_argument _ ->
+                raise (Browser_failure (sprintf "unsupported uri: %s" txt)))
+        in
+        self#_load entry;
+        self#_historyAdd entry
+      end
+
       (** {2 methods used by constructor only} *)
 
     method win = win
@@ -583,5 +652,5 @@ let mathViewer () =
     method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
       
     method show_uri_list ?(reuse=false) ~entry l =
-      (self#get_browser reuse)#loadList l entry
+      (self#get_browser reuse)#load entry
   end