Inteface improvement: the "Edit Aliases..." menu entry now opens a window where

aliases may be entered and modified. I am now going to remove aliases
declaration from the CIC textual parser.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 808caac082c692b0c6dade5159730e6b283d4be7..f6e31d0a47c0c7e2472eb78a47f5aba4b7ca0023 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -153,26 +153,31 @@ Arg.parse argspec ignore ""
 
 (* MISC FUNCTIONS *)
 
+exception IllFormedUri of string;;
+
 let cic_textual_parser_uri_of_string uri' =
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
-  CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
-  if String.sub uri' (String.length uri' - 4) 4 = ".var" then
-   CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ try
+  (* Constant *)
+  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
   else
-   (try
-     (* Inductive Type *)
-     let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
-      CicTextualParser0.IndTyUri (uri'',typeno)
-    with
-     _ ->
-      (* Constructor of an Inductive Type *)
-      let uri'',typeno,consno =
-       CicTextualLexer.indconuri_of_uri uri'
-      in
-       CicTextualParser0.IndConUri (uri'',typeno,consno)
-   )
+   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+   else
+    (try
+      (* Inductive Type *)
+      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+       CicTextualParser0.IndTyUri (uri'',typeno)
+     with
+      _ ->
+       (* Constructor of an Inductive Type *)
+       let uri'',typeno,consno =
+        CicTextualLexer.indconuri_of_uri uri'
+       in
+        CicTextualParser0.IndConUri (uri'',typeno,consno)
+    )
+ with
+  _ -> raise (IllFormedUri uri')
 ;;
 
 let term_of_cic_textual_parser_uri uri =
@@ -786,25 +791,75 @@ let load () =
 ;;
 
 let edit_aliases () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let chosen = ref false in
+ let window =
+  GWindow.window
+   ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
+ let vbox =
+  GPack.vbox ~border_width:0 ~packing:window#add () in
+ let scrolled_window =
+  GBin.scrolled_window ~border_width:10
+   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let input = GEdit.text ~editable:true ~width:400 ~height:100
+   ~packing:scrolled_window#add () in
+ let hbox =
+  GPack.hbox ~border_width:0
+   ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+  GButton.button ~label:"Ok"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+  GButton.button ~label:"Cancel"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+  (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
  let dom,resolve_id = !id_to_uris in
-  let inputlen = inputt#length in
-   inputt#delete_text 0 inputlen ;
-   let _ =
-    inputt#insert_text ~pos:0
-     (String.concat "\n"
-       (List.map
-         (function v ->
-           let uri =
-            match resolve_id v with
-               None -> assert false
-             | Some uri -> uri
-           in
-            "alias " ^ v ^ " " ^
-              (string_of_cic_textual_parser_uri uri)
-         ) dom))
+  ignore
+   (input#insert_text ~pos:0
+    (String.concat "\n"
+      (List.map
+        (function v ->
+          let uri =
+           match resolve_id v with
+              None -> assert false
+            | Some uri -> uri
+          in
+           "alias " ^ v ^ " " ^
+             (string_of_cic_textual_parser_uri uri)
+        ) dom))) ;
+  window#show () ;
+  GMain.Main.main () ;
+  if !chosen then
+   let dom,resolve_id =
+    let inputtext = input#get_chars 0 input#length in
+    let regexpr =
+     let alfa = "[a-zA-Z_-]" in
+     let digit = "[0-9]" in
+     let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
+     let blanks = "\( \|\t\|\n\)+" in
+     let nonblanks = "[^ \t\n]+" in
+     let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
+      Str.regexp
+       ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
+    in
+     let rec aux n =
+      try
+       let n' = Str.search_forward regexpr inputtext n in
+        let id = Str.matched_group 2 inputtext in
+        let uri =
+         cic_textual_parser_uri_of_string
+          ("cic:" ^ (Str.matched_group 5 inputtext))
+        in
+         let dom,resolve_id = aux (n' + 1) in
+          id::dom,(function id'-> if id = id' then Some uri else resolve_id id')
+      with
+       Not_found -> empty_id_to_uris
+     in
+      aux 0
    in
-    id_to_uris := empty_id_to_uris
+    id_to_uris := dom,resolve_id
 ;;
 
 let proveit () =