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 *)
=
(*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 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
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
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 =
;;
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 =
| 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>") ;
;;
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
) 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
tactic expr ;
refresh_sequent notebook ;
refresh_proof output ;
- inputt#delete_text 0 inputlen
+ inputt#reset
with
RefreshSequentException e ->
output_html outputhtml
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
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
| 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
~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 ->
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 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) () =
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 ;
"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 ->
(* 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 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);
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 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 _ =
~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(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;;
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