X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=3774ed0d7b8c5e55fe03677945aa3d343685c245;hb=a3ea60dba4a46e32ab70a0ebda36367a8186a59f;hp=93924b9ada6a71331a28f5cb7002844dc88659c6;hpb=7d44fa19cb262a8180a9e48d210311bf0732dbb3;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 93924b9ad..3774ed0d7 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -53,6 +53,7 @@ let htmlheader_and_content = ref htmlheader;;
let current_cic_infos = ref None;;
let current_goal_infos = ref None;;
+let current_scratch_infos = ref None;;
(* MISC FUNCTIONS *)
@@ -226,9 +227,11 @@ let mml_of_cic_term term =
let sequent_doc =
Xml2Gdome.document_of_xml domImpl sequent_gdome
in
- applyStylesheets sequent_doc sequent_styles sequent_args
- (*CSC: magari prima o poi serve*)
- (*current_scratch_infos := Some (ids_to_terms,ids_to_father_ids)*)
+ let res =
+ applyStylesheets sequent_doc sequent_styles sequent_args ;
+ in
+ current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
+ res
;;
let output_html outputhtml msg =
@@ -411,6 +414,43 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
("
No term selected
")
;;
+let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ 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 savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match mmlwidget#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.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_scratch_infos with
+ (* term is the whole goal in the scratch_area *)
+ Some (term,ids_to_terms, ids_to_father_ids) ->
+ let id = xpath in
+ let expr = tactic term (Hashtbl.find ids_to_terms id) in
+ let mml = mml_of_cic_term expr in
+ scratch_window#show () ;
+ scratch_window#mmlwidget#load_tree ~dom:mml
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
+ end
+ | None ->
+ output_html outputhtml
+ ("No term selected
")
+;;
+
let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
let exact rendering_window =
call_tactic_with_input ProofEngine.exact rendering_window
@@ -441,6 +481,19 @@ let change rendering_window =
;;
+let whd_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
+ scratch_window
+;;
+let reduce_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
+ scratch_window
+;;
+let simpl_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
+ scratch_window
+;;
+
(**********************)
@@ -582,6 +635,7 @@ let state rendering_window () =
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
@@ -614,9 +668,9 @@ let check rendering_window scratch_window () =
| Some expr ->
try
let ty = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
- let mml = mml_of_cic_term ty in
+ let mml = mml_of_cic_term (Cic.Cast (expr,ty)) in
scratch_window#show () ;
- scratch_window#display ~dom:mml
+ scratch_window#mmlwidget#load_tree ~dom:mml
with
e ->
print_endline ("? " ^ CicPp.ppterm expr) ;
@@ -624,7 +678,8 @@ let check rendering_window scratch_window () =
done
with
CicTextualParser0.Eof ->
- inputt#delete_text 0 inputlen
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
| e ->
output_html outputhtml
("" ^ Printexc.to_string e ^ "
") ;
@@ -777,16 +832,38 @@ end;;
(* Scratch window *)
-class scratch_window () =
+class scratch_window outputhtml =
let window =
GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let vbox =
+ GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let whdb =
+ GButton.button ~label:"Whd"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let reduceb =
+ GButton.button ~label:"Reduce"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let simplb =
+ GButton.button ~label:"Simpl"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
let mmlwidget =
- GMathView.math_view ~packing:(window#add) ~width:400 ~height:280 () in
+ GMathView.math_view
+ ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
- method display = mmlwidget#load_tree
+ method outputhtml = outputhtml
+ method mmlwidget = mmlwidget
method show () = window#misc#hide () ; window#show ()
initializer
- ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
+ ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
+ ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
+ ignore(whdb#connect#clicked (whd_in_scratch self)) ;
+ ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
+ ignore(simplb#connect#clicked (simpl_in_scratch self))
end;;
(* Main window *)
@@ -881,7 +958,7 @@ class rendering_window output proofw (label : GMisc.label) =
~width:400 ~height: 200
~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
~show:true () in
- let scratch_window = new scratch_window () in
+ let scratch_window = new scratch_window outputhtml in
object(self)
method outputhtml = outputhtml
method oldinputt = oldinputt