(* A WIDGET TO ENTER CIC TERMS *)
-class term_editor ?packing ?width ?height ?changed_callback () =
+class term_editor ?packing ?width ?height ?isnotempty_callback () =
let input = GEdit.text ~editable:true ?width ?height ?packing () in
let _ =
- match changed_callback with
+ match isnotempty_callback with
None -> ()
| Some callback ->
ignore(input#connect#changed (function () -> callback (input#length > 0)))
=
(*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
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 *)
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
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,
| _ -> 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
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
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
let non_empty_type = ref false in
let window =
GWindow.window
- ~width:600 ~modal:true ~title:"New Proof or Definition" ~border_width:2 () in
+ ~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
(* moved here to have visibility of the ok button *)
let newinputt =
new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
- ~changed_callback:
+ ~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
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
let html =
" <h1>Backward Query: </h1>" ^
" <h2>Levels: </h2> " ^
- MQueryGenerator.string_of_levels
- (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+ MQueryLevels.string_of_levels
+ (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
" <pre>" ^ get_last_query result ^ "</pre>"
in
output_html outputhtml html ;
(* Scratch window *)
-class scratch_window outputhtml =
+class scratch_window =
let window =
GWindow.window ~title:"MathML viewer" ~border_width:2 () in
let vbox =
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
(* 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 *)
let export_to_postscript_menu_item =
begin
let _ =
- factory1#add_item "New Proof or Definition" ~key:GdkKeysyms._N
+ factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
~callback:new_proof
in
let reopen_menu_item =
~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
+ (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
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 =
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
~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 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
+ ~packing:frame#add () in
let inputt =
- new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in
+ 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 _ =
~border_width:20
~packing:frame#add
~show:true () in
- let scratch_window = new scratch_window outputhtml in
object
method outputhtml = outputhtml
method inputt = inputt
set_settings_window settings_window ;
set_outputhtml outputhtml ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
- ignore(checkb#connect#clicked (check scratch_window)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
end;;
let _ =
if !usedb then
- Mqint.init "dbname=helm_mowgli" ;
-(* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
+ begin
+ Mqint.set_database Mqint.postgres_db ;
+ (* Mqint.init "dbname=helm_mowgli" ; *)
+ Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
+ end ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
if !usedb then Mqint.close ();
projects / helm.git / blobdiff