X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=800e69aa07b485cd326638ad3b3f5ba33caee01c;hb=f233601294e39910180eeadbf39eca5c79329b3f;hp=eb02cb07f8e88b9a69204ab8cdfd637a88b9472d;hpb=18ce84578a8aed3b1320ec0b42507f26fc5e3ca4;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index eb02cb07f..800e69aa0 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -300,7 +300,6 @@ let call_tactic_with_input tactic rendering_window () =
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen
| e ->
-prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
output_html outputhtml
("
" ^ Printexc.to_string e ^ "
");
ProofEngine.proof := savedproof ;
@@ -335,7 +334,6 @@ let call_tactic_with_goal_input tactic rendering_window () =
| None -> assert false (* "ERROR: No current term!!!" *)
with
e ->
- prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
output_html outputhtml
("" ^ Printexc.to_string e ^ "
")
end
@@ -405,7 +403,6 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
| None -> assert false (* "ERROR: No current term!!!" *)
with
e ->
-prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
output_html outputhtml
("" ^ Printexc.to_string e ^ "
")
end
@@ -481,31 +478,34 @@ let save rendering_window () =
let proveit rendering_window () =
let module L = LogicalOperations in
let module G = Gdome in
- match rendering_window#output#get_selection with
- Some node ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- (*CSC: OCAML DIVERGE
- ((element : G.element)#getAttributeNS
- *)
- ~namespaceURI:helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match !current_cic_infos with
- Some (ids_to_terms, ids_to_father_ids) ->
- let id = xpath in
- if L.to_sequent id ids_to_terms ids_to_father_ids then
- refresh_proof rendering_window#output ;
- refresh_sequent rendering_window#proofw
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
- end
- | None -> assert false (* "ERROR: No selection!!!" *)
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ match rendering_window#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids) ->
+ let id = xpath in
+ if L.to_sequent id ids_to_terms ids_to_father_ids then
+ refresh_proof rendering_window#output ;
+ refresh_sequent rendering_window#proofw
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
;;
exception NotADefinition;;
@@ -576,12 +576,12 @@ let state rendering_window () =
inputt#delete_text 0 inputlen ;
ignore(oldinputt#insert_text input oldinputt#length)
| e ->
- print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
") ;
;;
let check rendering_window scratch_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
- let oldinputt = (rendering_window#oldinputt : GEdit.text) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let output = (rendering_window#output : GMathView.math_view) in
let proofw = (rendering_window#proofw : GMathView.math_view) in
@@ -589,13 +589,13 @@ let check rendering_window scratch_window () =
let input = inputt#get_chars 0 inputlen ^ "\n" in
let curi,metasenv =
match !ProofEngine.proof with
- None -> assert false
+ None -> UriManager.uri_of_string "cic:/dummy.con", []
| Some (curi,metasenv,_,_) -> curi,metasenv
in
let ciccontext,names_context =
let context =
match !ProofEngine.goal with
- None -> assert false
+ None -> []
| Some (_,(ctx,_)) -> ctx
in
ProofEngine.cic_context_of_context context,
@@ -624,10 +624,10 @@ let check rendering_window scratch_window () =
done
with
CicTextualParser0.Eof ->
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length)
+ inputt#delete_text 0 inputlen
| e ->
- print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
") ;
;;
let choose_selection
@@ -786,7 +786,7 @@ object(self)
method display = mmlwidget#load_tree
method show = window#show
initializer
- ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
+ ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
end;;
(* Main window *)