(* 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
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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ )) ;
+ 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 ;
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
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);
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
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))
projects / helm.git / commitdiff