X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8ec91964edff51159a58bb197e2d57f5bdc31aa2;hb=5379335718a93d3e933d9bfdc0dd85f00983bc21;hp=43d8ddf15b7cb5b4149914f4926f0c3540e9390a;hpb=5a68517d961343d0b3454764af6082bed35b7311;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 43d8ddf15..8ec91964e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -150,6 +150,32 @@ let argspec =
 in
 Arg.parse argspec ignore ""
 
+(* A WIDGET TO ENTER CIC TERMS *)
+
+class term_editor ?packing ?width ?height ?isnotempty_callback () =
+ let input = GEdit.text ~editable:true ?width ?height ?packing () in
+ let _ =
+  match isnotempty_callback with
+     None -> ()
+   | Some callback ->
+      ignore(input#connect#changed (function () -> callback (input#length > 0)))
+ in
+object(self)
+ method coerce = input#coerce
+ method reset =
+  input#delete_text 0 input#length
+ (* CSC: txt is now a string, but should be of type Cic.term *)
+ method set_term txt =
+  self#reset ;
+  ignore ((input#insert_text txt) ~pos:0)
+ (* CSC: this method should disappear *)
+ method get_as_string =
+  input#get_chars 0 input#length
+ 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 *)
 
@@ -504,11 +530,12 @@ let
 =
 (*CSC: ????????????????? *)
  let xml, bodyxml =
-  Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
  in
  let xmlinnertypes =
-  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
-   ~ids_to_inner_types
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
  in
   let input =
    match bodyxml with
@@ -525,6 +552,55 @@ let
     output
 ;;
 
+let
+ save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
+=
+ let name =
+  let struri = UriManager.string_of_uri uri in
+  let idx = (String.rindex struri '/') + 1 in
+   String.sub struri idx (String.length struri - idx)
+ in
+  let path = pathname ^ "/" ^ name in
+  let xml, bodyxml =
+   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+    annobj 
+  in
+  let xmlinnertypes =
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+    ~ask_dtd_to_the_getter:false
+  in
+   (* innertypes *)
+   let innertypesuri = UriManager.innertypesuri_of_uri uri in
+    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+    Getter.register innertypesuri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri innertypesuri) ^ ".xml"
+     ) ;
+    (* constant type / variable / mutual inductive types definition *)
+    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+    Getter.register uri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".xml"
+     ) ;
+    match bodyxml with
+       None -> ()
+     | Some bodyxml' ->
+        (* constant body *)
+        let bodyuri =
+         match UriManager.bodyuri_of_uri uri with
+            None -> assert false
+          | Some bodyuri -> bodyuri
+        in
+         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+         Getter.register bodyuri
+          (Configuration.annotations_url ^
+            Str.replace_first (Str.regexp "^cic:") ""
+             (UriManager.string_of_uri bodyuri) ^ ".xml"
+          )
+;;
+
 
 (* CALLBACKS *)
 
@@ -665,6 +741,15 @@ let mml_of_cic_term metano term =
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
+let pathname_of_annuri uristring =
+ Configuration.annotations_dir ^    
+  Str.replace_first (Str.regexp "^cic:") "" uristring
+;;
+
+let make_dirs dirpath =
+ ignore (Unix.system ("mkdir -p " ^ dirpath))
+;;
+
 let qed () =
  match !ProofEngine.proof with
     None -> assert false
@@ -687,6 +772,12 @@ let qed () =
            ids_to_inner_types
          in
           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
+          !qed_set_sensitive false ;
+          (* let's save the theorem and register it to the getter *) 
+          let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
+          make_dirs pathname ;
+          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
+           pathname ;
           current_cic_infos :=
            Some
             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
@@ -697,12 +788,6 @@ let qed () =
   | _ -> raise OpenConjecturesStillThere
 ;;
 
-(*????
-let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
-let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
-*)
-let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
-
 let save () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   match !ProofEngine.proof with
@@ -716,7 +801,10 @@ let save () =
         Cic2acic.acic_object_of_cic_object currentproof
        in
         let xml, bodyxml =
-         match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
+         match
+          Cic2Xml.print_object uri ~ids_to_inner_sorts
+           ~ask_dtd_to_the_getter:true acurrentproof
+         with
             xml,Some bodyxml -> xml,bodyxml
           | _,None -> assert false
         in
@@ -748,27 +836,33 @@ let load () =
  let output = ((rendering_window ())#output : GMathView.math_view) in
  let notebook = (rendering_window ())#notebook in
   try
-   let uri = UriManager.uri_of_string "cic:/dummy.con" in
-    match CicParser.obj_of_xml prooffiletype (Some prooffile) with
-       Cic.CurrentProof (_,metasenv,bo,ty,_) ->
-        typecheck_loaded_proof metasenv bo ty ;
-        ProofEngine.proof :=
-         Some (uri, metasenv, bo, ty) ;
-        ProofEngine.goal :=
-         (match metasenv with
-             [] -> None
-           | (metano,_,_)::_ -> Some metano
-         ) ;
-        refresh_proof output ;
-        refresh_sequent notebook ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof type loaded from " ^
-            prooffiletype ^ "</h1>") ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof body loaded from " ^
-            prooffile ^ "</h1>") ;
-        !save_set_sensitive true
-     | _ -> assert false
+   match 
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+     "Choose an URI:"
+   with
+      None -> raise NoChoice
+    | Some uri0 ->
+       let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
+        match CicParser.obj_of_xml prooffiletype (Some prooffile) with
+           Cic.CurrentProof (_,metasenv,bo,ty,_) ->
+            typecheck_loaded_proof metasenv bo ty ;
+            ProofEngine.proof :=
+             Some (uri, metasenv, bo, ty) ;
+            ProofEngine.goal :=
+             (match metasenv with
+                 [] -> None
+               | (metano,_,_)::_ -> Some metano
+             ) ;
+            refresh_proof output ;
+            refresh_sequent notebook ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof type loaded from " ^
+                prooffiletype ^ "</h1>") ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof body loaded from " ^
+                prooffile ^ "</h1>") ;
+            !save_set_sensitive true
+         | _ -> assert false
   with
      RefreshSequentException e ->
       output_html outputhtml
@@ -1052,7 +1146,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 +1155,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
@@ -1293,43 +1386,125 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr =
      mk_metasenv_and_expr resolve_id'
 ;;
 
-let state () =
- let inputt = ((rendering_window ())#inputt : GEdit.text) in
+exception UriAlreadyInUse;;
+exception NotAUriToAConstant;;
+
+let new_proof () =
+ 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 ->
+
+ let chosen = ref false in
+ let get_parsed = ref (function _ -> assert false) in
+ let get_uri = ref (function _ -> assert false) in
+ let non_empty_type = ref false in
+ let window =
+  GWindow.window
+   ~width:600 ~modal:true ~title:"New Proof or Definition"
+   ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox =
+  GPack.hbox ~border_width:0
+   ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+  GMisc.label ~text:"Enter the URI for the new theorem or definition:"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let uri_entry =
+  GEdit.entry ~editable:true
+   ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let hbox1 =
+  GPack.hbox ~border_width:0
+   ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+  GMisc.label ~text:"Enter the theorem or definition type:"
+   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+  GBin.scrolled_window ~border_width:5
+   ~packing:(vbox#pack ~expand:true ~padding:0) () in
+ (* the content of the scrolled_window is moved below (see comment) *)
+ 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 _ = okb#misc#set_sensitive false in
+ let cancelb =
+  GButton.button ~label:"Cancel"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* moved here to have visibility of the ok button *)
+ let newinputt =
+  new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
+   ~isnotempty_callback:
+    (function b ->
+      non_empty_type := b ;
+      okb#misc#set_sensitive (b && uri_entry#text <> ""))
+ in
+ let _ =
+  newinputt#set_term inputt#get_as_string ;
+  inputt#reset in
+ let _ =
+  uri_entry#connect#changed
+   (function () ->
+     okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+  (okb#connect#clicked
+    (function () ->
+      chosen := true ;
+      try
+       let parsed = newinputt#get_term [] [] in
+       let uristr = "cic:" ^ uri_entry#text in
+       let uri = UriManager.uri_of_string uristr in
+        if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
+         raise NotAUriToAConstant
+        else
+         begin
+          try
+           ignore (Getter.resolve uri) ;
+           raise UriAlreadyInUse
+          with
+           Getter.Unresolved ->
+            get_parsed := (function () -> parsed) ;
+            get_uri := (function () -> uri) ; 
+            window#destroy ()
+         end
+      with
+       e ->
         output_html outputhtml
          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+  )) ;
+ window#show () ;
+ GMain.Main.main () ;
+ if !chosen then
+  try
+   let dom,mk_metasenv_and_expr = !get_parsed () in
+    let metasenv,expr =
+     disambiguate_input [] [] dom mk_metasenv_and_expr
+    in
+     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
+      ProofEngine.proof :=
+       Some (!get_uri (), (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 +1521,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 +1545,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 +1601,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 +1626,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 +1634,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 +1717,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 +1734,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 +1754,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 +1765,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 ->
@@ -1651,7 +1798,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
  let module L = LogicalOperations in
  let module G = Gdome in
   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
-  let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
+  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
    match mmlwidget#get_selection with
@@ -1830,7 +1977,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 +2061,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 -> 
@@ -2078,7 +2224,7 @@ end;;
 
 (* Scratch window *)
 
-class scratch_window outputhtml =
+class scratch_window =
  let window =
   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
  let vbox =
@@ -2101,7 +2247,6 @@ class scratch_window outputhtml =
   GMathView.math_view
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
- method outputhtml = outputhtml
  method mmlwidget = mmlwidget
  method show () = window#misc#hide () ; window#show ()
  initializer
@@ -2317,12 +2462,15 @@ end
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
+ let scratch_window = new scratch_window in
  let window =
-  GWindow.window ~title:"MathML viewer" ~border_width:2
+  GWindow.window ~title:"MathML viewer" ~border_width:0
    ~allow_shrink:false () in
  let vbox_for_menu = GPack.vbox ~packing:window#add () in
  (* menus *)
- let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
+ let handle_box = GBin.handle_box ~border_width:2
+  ~packing:(vbox_for_menu#pack ~padding:0) () in
+ let menubar = GMenu.menu_bar ~packing:handle_box#add () in
  let factory0 = new GMenu.factory menubar in
  let accel_group = factory0#accel_group in
  (* file menu *)
@@ -2330,18 +2478,23 @@ class rendering_window output (notebook : notebook) =
  let factory1 = new GMenu.factory file_menu ~accel_group in
  let export_to_postscript_menu_item =
   begin
-   ignore
-    (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
-      ~callback:load) ;
-   let save_menu_item =
-    factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
+   let _ =
+    factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
+     ~callback:new_proof
    in
    let reopen_menu_item =
     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
      ~callback:open_
    in
    let qed_menu_item =
-    factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
+    factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
+   ignore (factory1#add_separator ()) ;
+   ignore
+    (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
+      ~callback:load) ;
+   let save_menu_item =
+    factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
+   in
    ignore
     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
    ignore (!save_set_sensitive false);
@@ -2349,15 +2502,15 @@ class rendering_window output (notebook : notebook) =
    ignore (!qed_set_sensitive false);
    ignore (factory1#add_separator ()) ;
    let export_to_postscript_menu_item =
-    factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
+    factory1#add_item "Export to PostScript..."
      ~callback:(export_to_postscript output) in
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
+    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
    export_to_postscript_menu_item
   end in
  (* edit menu *)
- let edit_menu = factory0#add_submenu "Edit current proof" in
+ let edit_menu = factory0#add_submenu "Edit Current Proof" in
  let factory2 = new GMenu.factory edit_menu ~accel_group in
  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
  let proveit_menu_item =
@@ -2375,6 +2528,13 @@ class rendering_window output (notebook : notebook) =
     focus_menu_item#misc#set_sensitive b
  in
  let _ = !focus_and_proveit_set_sensitive false in
+ (* edit term menu *)
+ let edit_term_menu = factory0#add_submenu "Edit Term" in
+ let factory5 = new GMenu.factory edit_term_menu ~accel_group in
+ let check_menu_item =
+  factory5#add_item "Check Term" ~key:GdkKeysyms._C
+   ~callback:(check scratch_window) in
+ let _ = check_menu_item#misc#set_sensitive false in
  (* search menu *)
  let settings_menu = factory0#add_submenu "Search" in
  let factory4 = new GMenu.factory settings_menu ~accel_group in
@@ -2407,23 +2567,14 @@ class rendering_window output (notebook : notebook) =
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let _ = scrolled_window0#add output#coerce in
  let frame =
-  GBin.frame ~label:"Term input"
+  GBin.frame ~label:"Insert Term"
    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let vbox' =
-  GPack.vbox ~packing:frame#add () in
- let hbox4 =
-  GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
- let stateb =
-  GButton.button ~label:"State"
-   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
- let checkb =
-  GButton.button ~label:"Check"
-   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  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
+   ~packing:frame#add () in
+ let inputt =
+  new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
+   ~isnotempty_callback:check_menu_item#misc#set_sensitive in
  let vboxl =
   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
  let _ =
@@ -2438,7 +2589,6 @@ class rendering_window output (notebook : notebook) =
    ~border_width:20
    ~packing:frame#add
    ~show:true () in
- let scratch_window = new scratch_window outputhtml in
 object
  method outputhtml = outputhtml
  method inputt = inputt
@@ -2462,8 +2612,6 @@ object
   set_settings_window settings_window ;
   set_outputhtml outputhtml ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
-  ignore(stateb#connect#clicked state) ;
-  ignore(checkb#connect#clicked (check scratch_window)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
 end;;