Code clean-up: the widget in the lower-left corner is now a widget to input

CIC terms, featuring the following methods:
* get_term
* set_term  (issue: what should be its type? So far the input is a string)
* reset

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 43d8ddf15b7cb5b4149914f4926f0c3540e9390a..7efc515fa9b086608935d2cb71ffce358d2015b7 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -150,6 +150,22 @@ let argspec =
 in
 Arg.parse argspec ignore ""
 
+(* A WIDGET TO ENTER CIC TERMS *)
+
+class term_editor ?packing ?width ?height () =
+ let input = GEdit.text ~editable:true ?width ?height ?packing () in
+object(self)
+ method coerce = input#coerce
+ method reset =
+  input#delete_text 0 input#length
+ method set_term txt =
+  self#reset ;
+  ignore ((input#insert_text txt) ~pos:0)
+ method get_term ~context ~metasenv =
+  let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
+   CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
+end
+;;
 
 (* MISC FUNCTIONS *)
 
@@ -1052,7 +1068,7 @@ let locate_callback id =
 ;;
 
 let locate () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
    try
     match
@@ -1061,8 +1077,7 @@ let locate () =
        None -> raise NoChoice
      | Some input ->
         let uri = locate_callback input in
-         inputt#delete_text 0 inputt#length ;
-         ignore ((inputt#insert_text uri) ~pos:0)
+         inputt#set_term uri
    with
     e ->
      output_html outputhtml
@@ -1294,42 +1309,37 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr =
 ;;
 
 let state () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let output = ((rendering_window ())#output : GMathView.math_view) in
  let notebook = (rendering_window ())#notebook in
-  let inputlen = inputt#length in
-  let input = inputt#get_chars 0 inputlen ^ "\n" in
-   (* Do something interesting *)
-   let lexbuf = Lexing.from_string input in
-    try
-     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
-    with
-       RefreshSequentException e ->
-        output_html outputhtml
-         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-          "sequent: " ^ Printexc.to_string e ^ "</h1>")
-     | RefreshProofException e ->
-        output_html outputhtml
-         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-          "proof: " ^ Printexc.to_string e ^ "</h1>")
-     | e ->
-        output_html outputhtml
-         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+  try
+   let dom,mk_metasenv_and_expr = inputt#get_term [] [] 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#reset
+  with
+     RefreshSequentException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+   | RefreshProofException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e ^ "</h1>")
+   | e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 let check_term_in_scratch scratch_window metasenv context expr = 
@@ -1346,14 +1356,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
 ;;
 
 let check scratch_window () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let inputlen = inputt#length in
-  let input = inputt#get_chars 0 inputlen ^ "\n" in
-  let curi,metasenv =
+  let metasenv =
    match !ProofEngine.proof with
-      None -> UriManager.uri_of_string "cic:/dummy.con", []
-    | Some (curi,metasenv,_,_) -> curi,metasenv
+      None -> []
+    | Some (_,metasenv,_,_) -> metasenv
   in
   let context,names_context =
    let context =
@@ -1372,20 +1380,16 @@ let check scratch_window () =
        | None -> None
      ) context
   in
-   let lexbuf = Lexing.from_string input in
-    try
-     let dom,mk_metasenv_and_expr =
-      CicTextualParserContext.main names_context metasenv CicTextualLexer.token
-       lexbuf
+   try
+    let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
+     let (metasenv',expr) =
+      disambiguate_input context metasenv dom mk_metasenv_and_expr
      in
-      let (metasenv',expr) =
-       disambiguate_input context metasenv dom mk_metasenv_and_expr
-      in
-       check_term_in_scratch scratch_window metasenv' context expr
-    with
-     e ->
-      output_html outputhtml
-       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+      check_term_in_scratch scratch_window metasenv' context expr
+   with
+    e ->
+     output_html outputhtml
+      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
 
@@ -1432,23 +1436,14 @@ let call_tactic_with_input tactic () =
  let notebook = (rendering_window ())#notebook in
  let output = ((rendering_window ())#output : GMathView.math_view) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
  let savedproof = !ProofEngine.proof in
  let savedgoal  = !ProofEngine.goal in
-(*CSC: Gran cut&paste da sotto... *)
-  let inputlen = inputt#length in
-  let input = inputt#get_chars 0 inputlen ^ "\n" in
-   let lexbuf = Lexing.from_string input in
-   let curi =
-    match !ProofEngine.proof with
-       None -> assert false
-     | Some (curi,_,_,_) -> curi
-   in
-   let uri,metasenv,bo,ty =
-    match !ProofEngine.proof with
-       None -> assert false
-     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-   in
+  let uri,metasenv,bo,ty =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+  in
    let canonical_context =
     match !ProofEngine.goal with
        None -> assert false
@@ -1466,9 +1461,7 @@ let call_tactic_with_input tactic () =
      ) canonical_context
    in
     try
-     let dom,mk_metasenv_and_expr =
-      CicTextualParserContext.main context metasenv CicTextualLexer.token lexbuf
-     in
+     let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
       let (metasenv',expr) =
        disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
       in
@@ -1476,7 +1469,7 @@ let call_tactic_with_input tactic () =
        tactic expr ;
        refresh_sequent notebook ;
        refresh_proof output ;
-       inputt#delete_text 0 inputlen
+       inputt#reset
     with
        RefreshSequentException e ->
         output_html outputhtml
@@ -1559,7 +1552,7 @@ let call_tactic_with_input_and_goal_input tactic () =
   let notebook = (rendering_window ())#notebook in
   let output = ((rendering_window ())#output : GMathView.math_view) in
   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let inputt = ((rendering_window ())#inputt : GEdit.text) in
+  let inputt = ((rendering_window ())#inputt : term_editor) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
    match notebook#proofw#get_selection with
@@ -1576,20 +1569,11 @@ let call_tactic_with_input_and_goal_input tactic () =
           match !current_goal_infos with
              Some (ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
-               (* Let's parse the input *)
-               let inputlen = inputt#length in
-               let input = inputt#get_chars 0 inputlen ^ "\n" in
-                let lexbuf = Lexing.from_string input in
-                let curi =
-                 match !ProofEngine.proof with
-                    None -> assert false
-                  | Some (curi,_,_,_) -> curi
-                in
-                let uri,metasenv,bo,ty =
-                 match !ProofEngine.proof with
-                    None -> assert false
-                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-                in
+               let uri,metasenv,bo,ty =
+                match !ProofEngine.proof with
+                   None -> assert false
+                 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+               in
                 let canonical_context =
                  match !ProofEngine.goal with
                     None -> assert false
@@ -1605,9 +1589,7 @@ let call_tactic_with_input_and_goal_input tactic () =
                     | None -> None
                   ) canonical_context
                 in
-                 let dom,mk_metasenv_and_expr =
-                  CicTextualParserContext.main context metasenv
-                   CicTextualLexer.token lexbuf
+                 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
                  in
                   let (metasenv',expr) =
                    disambiguate_input canonical_context metasenv dom
@@ -1618,7 +1600,7 @@ let call_tactic_with_input_and_goal_input tactic () =
                     ~input:expr ;
                    refresh_sequent notebook ;
                    refresh_proof output ;
-                   inputt#delete_text 0 inputlen
+                   inputt#reset
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
             RefreshSequentException e ->
@@ -1830,7 +1812,7 @@ let open_ () =
 
 
 let searchPattern () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    let rec get_level ?(last_invalid=false) () =
@@ -1914,8 +1896,7 @@ let searchPattern () =
                 "Many lemmas can be successfully applied. Please, choose one:"
                uris'
              in
-              inputt#delete_text 0 inputt#length ;
-              ignore ((inputt#insert_text uri') ~pos:0) ;
+              inputt#set_term uri' ;
               apply ()
   with
    e -> 
@@ -2422,8 +2403,8 @@ class rendering_window output (notebook : notebook) =
  let scrolled_window1 =
   GBin.scrolled_window ~border_width:5
    ~packing:(vbox'#pack ~expand:true ~padding:0) () in
- let inputt = GEdit.text ~editable:true ~width:400 ~height:100
-   ~packing:scrolled_window1#add () in
+ let inputt =
+  new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in
  let vboxl =
   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
  let _ =