From: Claudio Sacerdoti Coen Date: Mon, 18 Nov 2002 17:23:45 +0000 (+0000) Subject: Interface improvement: X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=674691387a3d7d0055c100bfb0bc9e0dcb1dcd07;p=helm.git Interface improvement: * "State" button replaced with a menu item; * the URI is now requested to the user --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7efc515fa..2b5380e69 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -152,15 +152,25 @@ Arg.parse argspec ignore "" (* A WIDGET TO ENTER CIC TERMS *) -class term_editor ?packing ?width ?height () = +class term_editor ?packing ?width ?height ?changed_callback () = let input = GEdit.text ~editable:true ?width ?height ?packing () in + let _ = + match changed_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 @@ -1308,21 +1318,107 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = mk_metasenv_and_expr resolve_id' ;; -let state () = +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 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 () + ~changed_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 + ("

" ^ Printexc.to_string e ^ "

") ; + )) ; + window#show () ; + GMain.Main.main () ; + if !chosen then try - let dom,mk_metasenv_and_expr = inputt#get_term [] [] in + 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 - (UriManager.uri_of_string "cic:/dummy.con", - (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; ProofEngine.goal := Some 1 ; refresh_sequent notebook ; refresh_proof output ; @@ -2311,11 +2407,9 @@ 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 @@ -2323,6 +2417,13 @@ class rendering_window output (notebook : notebook) = in let qed_menu_item = factory1#add_item "Qed" ~key:GdkKeysyms._Q ~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); @@ -2394,9 +2495,6 @@ class rendering_window output (notebook : notebook) = 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 @@ -2443,7 +2541,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))