Aliases definition removed from the CIC textual parser.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f6e31d0a47c0c7e2472eb78a47f5aba4b7ca0023..43d8ddf15b7cb5b4149914f4926f0c3540e9390a 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -416,13 +416,6 @@ let get_last_query =
   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 ;;
 
-let register_alias (id,uri) =
- let dom,resolve_id = !id_to_uris in
-  id_to_uris :=
-   (if List.mem id dom then dom else id::dom),
-    function id' -> if id' = id then Some uri else resolve_id id'
-;;  
-
 let domImpl = Gdome.domImplementation ();;
 
 let parseStyle name =
@@ -853,7 +846,11 @@ let edit_aliases () =
           ("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')
+          if List.mem id dom then
+           dom,resolve_id
+          else
+           id::dom,
+            (function id' -> if id = id' then Some uri else resolve_id id')
       with
        Not_found -> empty_id_to_uris
      in
@@ -1306,30 +1303,23 @@ let state () =
    (* Do something interesting *)
    let lexbuf = Lexing.from_string input in
     try
-     while true do
-      (* Execute the actions *)
-      match
-       CicTextualParserContext.main [] [] CicTextualLexer.token
-        lexbuf register_alias
-      with
-         None -> ()
-       | Some (dom,mk_metasenv_and_expr) ->
-          let metasenv,expr =
-           disambiguate_input [] [] dom mk_metasenv_and_expr
-          in
-           let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
-            ProofEngine.proof :=
-             Some (UriManager.uri_of_string "cic:/dummy.con",
-                    (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
-            ProofEngine.goal := Some 1 ;
-            refresh_sequent notebook ;
-            refresh_proof output ;
-            !save_set_sensitive true
-     done
-    with
-       CicTextualParser0.Eof ->
+     let  dom,mk_metasenv_and_expr =
+      CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+     in
+      let metasenv,expr =
+       disambiguate_input [] [] dom mk_metasenv_and_expr
+      in
+       let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
+        ProofEngine.proof :=
+         Some (UriManager.uri_of_string "cic:/dummy.con",
+                (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
+        ProofEngine.goal := Some 1 ;
+        refresh_sequent notebook ;
+        refresh_proof output ;
+        !save_set_sensitive true ;
         inputt#delete_text 0 inputlen
-     | RefreshSequentException e ->
+    with
+       RefreshSequentException e ->
         output_html outputhtml
          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
           "sequent: " ^ Printexc.to_string e ^ "</h1>")
@@ -1384,24 +1374,18 @@ let check scratch_window () =
   in
    let lexbuf = Lexing.from_string input in
     try
-     while true do
-      (* Execute the actions *)
-      match
-       CicTextualParserContext.main names_context metasenv CicTextualLexer.token
-        lexbuf register_alias
-      with
-         None -> ()
-       | Some (dom,mk_metasenv_and_expr) ->
-          let (metasenv',expr) =
-           disambiguate_input context metasenv dom mk_metasenv_and_expr
-          in
-           check_term_in_scratch scratch_window metasenv' context expr
-     done
+     let dom,mk_metasenv_and_expr =
+      CicTextualParserContext.main names_context metasenv CicTextualLexer.token
+       lexbuf
+     in
+      let (metasenv',expr) =
+       disambiguate_input context metasenv dom mk_metasenv_and_expr
+      in
+       check_term_in_scratch scratch_window metasenv' context expr
     with
-       CicTextualParser0.Eof -> ()
-     | e ->
-       output_html outputhtml
-        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+     e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 
@@ -1482,26 +1466,19 @@ let call_tactic_with_input tactic () =
      ) canonical_context
    in
     try
-     while true do
-      match
-       CicTextualParserContext.main context metasenv CicTextualLexer.token
-        lexbuf register_alias
-      with
-         None -> ()
-       | Some (dom,mk_metasenv_and_expr) ->
-          let (metasenv',expr) =
-           disambiguate_input canonical_context metasenv dom
-            mk_metasenv_and_expr
-          in
-           ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-           tactic expr ;
-           refresh_sequent notebook ;
-           refresh_proof output
-     done
+     let dom,mk_metasenv_and_expr =
+      CicTextualParserContext.main context metasenv CicTextualLexer.token lexbuf
+     in
+      let (metasenv',expr) =
+       disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
+      in
+       ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+       tactic expr ;
+       refresh_sequent notebook ;
+       refresh_proof output ;
+       inputt#delete_text 0 inputlen
     with
-       CicTextualParser0.Eof ->
-        inputt#delete_text 0 inputlen
-     | RefreshSequentException e ->
+       RefreshSequentException e ->
         output_html outputhtml
          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
@@ -1628,29 +1605,20 @@ let call_tactic_with_input_and_goal_input tactic () =
                     | None -> None
                   ) canonical_context
                 in
-                 begin
-                  try
-                   while true do
-                    match
-                     CicTextualParserContext.main context metasenv
-                      CicTextualLexer.token lexbuf register_alias
-                    with
-                       None -> ()
-                     | Some (dom,mk_metasenv_and_expr) ->
-                        let (metasenv',expr) =
-                         disambiguate_input canonical_context metasenv dom
-                          mk_metasenv_and_expr
-                        in
-                         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
-                          ~input:expr ;
-                         refresh_sequent notebook ;
-                         refresh_proof output
-                   done
-                  with
-                     CicTextualParser0.Eof ->
-                      inputt#delete_text 0 inputlen
-                 end
+                 let dom,mk_metasenv_and_expr =
+                  CicTextualParserContext.main context metasenv
+                   CicTextualLexer.token lexbuf
+                 in
+                  let (metasenv',expr) =
+                   disambiguate_input canonical_context metasenv dom
+                    mk_metasenv_and_expr
+                  in
+                   ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+                   tactic ~goal_input:(Hashtbl.find ids_to_terms id)
+                    ~input:expr ;
+                   refresh_sequent notebook ;
+                   refresh_proof output ;
+                   inputt#delete_text 0 inputlen
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
             RefreshSequentException e ->