X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=58e785dec3ef37c5ff6cf8dfc4dad4d2819b3ba5;hb=87b98314c08ec399096f87a8e06d30234d7cc498;hp=ff93962131671546631ed081eaca21a5df7e5624;hpb=e07312820aa16f76e7584eb40d4e517c7d254667;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ff9396213..58e785dec 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -128,6 +128,16 @@ let set_outputhtml,outputhtml =
)
;;
+exception QedSetSensitiveNotInitialized;;
+let qed_set_sensitive =
+ ref (function _ -> raise QedSetSensitiveNotInitialized)
+;;
+
+exception SaveSetSensitiveNotInitialized;;
+let save_set_sensitive =
+ ref (function _ -> raise SaveSetSensitiveNotInitialized)
+;;
+
(* COMMAND LINE OPTIONS *)
let usedb = ref true
@@ -214,9 +224,7 @@ let check_window outputhtml uris =
let scrolled_window =
GBin.scrolled_window ~border_width:10
~packing:
- (notebook#append_page
- ~tab_label:((GMisc.label ~text:uri ())#coerce)
- )
+ (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
()
in
lazy
@@ -477,9 +485,11 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr =
in
aux dom' list_of_uris
in
- output_html (outputhtml ())
- ("
Disambiguation phase started: " ^
- string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
+ let tests_no = List.length resolve_ids in
+ if tests_no > 1 then
+ output_html (outputhtml ())
+ ("Disambiguation phase started: " ^
+ string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
(* now we select only the ones that generates well-typed terms *)
let resolve_ids' =
let rec filter =
@@ -648,6 +658,7 @@ let refresh_proof (output : GMathView.math_view) =
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
+ !qed_set_sensitive (List.length metasenv = 0) ;
(*CSC: Wrong: [] is just plainly wrong *)
uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
in
@@ -678,7 +689,7 @@ let refresh_sequent ?(empty_notebook=true) notebook =
None ->
if empty_notebook then
begin
- notebook#remove_all_pages ;
+ notebook#remove_all_pages ~skip_switch_page_event:false ;
notebook#set_empty_page
end
else
@@ -693,19 +704,29 @@ let refresh_sequent ?(empty_notebook=true) notebook =
let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
SequentPp.XmlPp.print_sequent metasenv currentsequent
in
- let sequent_doc =
- Xml2Gdome.document_of_xml domImpl sequent_gdome
- in
- let sequent_mml =
- applyStylesheets sequent_doc sequent_styles sequent_args
+ let regenerate_notebook () =
+ let skip_switch_page_event =
+ match metasenv with
+ (m,_,_)::_ when m = metano -> false
+ | _ -> true
in
+ notebook#remove_all_pages ~skip_switch_page_event ;
+ List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
+ in
if empty_notebook then
begin
- notebook#remove_all_pages ;
- List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
+ regenerate_notebook () ;
+ notebook#set_current_page ~may_skip_switch_page_event:false metano
+ end
+ else
+ begin
+ let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ notebook#set_current_page ~may_skip_switch_page_event:true metano;
+ notebook#proofw#load_tree ~dom:sequent_mml
end ;
- notebook#set_current_page metano ;
- notebook#proofw#load_tree ~dom:sequent_mml ;
current_goal_infos :=
Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
with
@@ -720,9 +741,11 @@ let metasenv =
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
+try
let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
raise (RefreshSequentException e)
+with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
;;
(*
@@ -1270,7 +1293,8 @@ let load () =
prooffiletype ^ "
") ;
output_html outputhtml
("Current proof body loaded from " ^
- prooffile ^ "
")
+ prooffile ^ "
") ;
+ !save_set_sensitive true
| _ -> assert false
with
RefreshSequentException e ->
@@ -1406,8 +1430,7 @@ let setgoal metano =
| Some (_,metasenv,_,_) -> metasenv
in
try
- ProofEngine.goal := Some metano ;
- refresh_sequent ~empty_notebook:false notebook ;
+ refresh_sequent ~empty_notebook:false notebook
with
RefreshSequentException e ->
output_html outputhtml
@@ -1486,6 +1509,7 @@ let state () =
ProofEngine.goal := Some 1 ;
refresh_sequent notebook ;
refresh_proof output ;
+ !save_set_sensitive true
done
with
CicTextualParser0.Eof ->
@@ -2006,28 +2030,56 @@ object(self)
end
;;
+class empty_page =
+ let vbox1 = GPack.vbox () in
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let proofw =
+ GMathView.math_view ~width:400 ~height:275
+ ~packing:(scrolled_window1#add) () in
+object(self)
+ method proofw = (assert false : GMathView.math_view)
+ method content = vbox1
+ method compute = (assert false : unit)
+end
+;;
+
+let empty_page = new empty_page;;
+
class notebook =
object(self)
val notebook = GPack.notebook ()
val pages = ref []
val mutable skip_switch_page_event = false
+ val mutable empty = true
method notebook = notebook
method add_page n =
let new_page = new page () in
+ empty <- false ;
pages := !pages @ [n,lazy (setgoal n),new_page] ;
notebook#append_page
~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
new_page#content#coerce
- method remove_all_pages =
- List.iter (function _ -> notebook#remove_page 0) !pages ;
+ method remove_all_pages ~skip_switch_page_event:skip =
+ if empty then
+ notebook#remove_page 0 (* let's remove the empty page *)
+ else
+ List.iter (function _ -> notebook#remove_page 0) !pages ;
pages := [] ;
- method set_current_page n =
+ skip_switch_page_event <- skip
+ method set_current_page ~may_skip_switch_page_event n =
let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
let new_page = notebook#page_num page#content#coerce in
- if new_page <> notebook#current_page then
+ if may_skip_switch_page_event && new_page <> notebook#current_page then
skip_switch_page_event <- true ;
notebook#goto_page new_page
- method set_empty_page = self#add_page (-1)
+ method set_empty_page =
+ empty <- true ;
+ pages := [] ;
+ notebook#append_page
+ ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
+ empty_page#content#coerce
method proofw =
let (_,_,page) = List.nth !pages notebook#current_page in
page#proofw
@@ -2039,7 +2091,8 @@ object(self)
skip_switch_page_event <- false ;
if not skip then
try
- let (_,setgoal,page) = List.nth !pages i in
+ let (metano,setgoal,page) = List.nth !pages i in
+ ProofEngine.goal := Some metano ;
Lazy.force (page#compute) ;
Lazy.force setgoal
with _ -> ()
@@ -2064,8 +2117,18 @@ class rendering_window output (notebook : notebook) =
let export_to_postscript_menu_item =
begin
ignore
- (factory1#add_item "Load" ~key:GdkKeysyms._L ~callback:load) ;
- ignore (factory1#add_item "Save" ~key:GdkKeysyms._S ~callback:save) ;
+ (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
+ let qed_menu_item =
+ factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
+ ignore
+ (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
+ ignore (!save_set_sensitive false);
+ ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
+ ignore (!qed_set_sensitive false);
ignore (factory1#add_separator ()) ;
let export_to_postscript_menu_item =
factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
@@ -2093,8 +2156,6 @@ class rendering_window output (notebook : notebook) =
proveit_menu_item#misc#set_sensitive b ;
focus_menu_item#misc#set_sensitive b
in
- let _ = factory2#add_separator () in
- let _ = factory2#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
let _ = !focus_and_proveit_set_sensitive false in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
@@ -2118,8 +2179,12 @@ class rendering_window output (notebook : notebook) =
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~padding:5) () in
let _ = scrolled_window0#add output#coerce in
+ let frame =
+ GBin.frame ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let vbox' =
+ GPack.vbox ~packing:frame#add () in
let hbox4 =
- GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ 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
@@ -2136,15 +2201,17 @@ class rendering_window output (notebook : notebook) =
GButton.button ~label:"SearchPattern"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let scrolled_window1 =
- GBin.scrolled_window ~border_width:10
- ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ 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
let vboxl =
GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
let _ =
vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
- let frame = GBin.frame ~packing:(vboxl#pack ~expand:true ~padding:5) () in
+ let frame =
+ GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
+ in
let outputhtml =
GHtml.xmhtml
~source:""
@@ -2167,7 +2234,6 @@ object
(* signal handlers here *)
ignore(output#connect#selection_changed
(function elem ->
- notebook#proofw#unload ;
choose_selection output elem ;
!focus_and_proveit_set_sensitive true
)) ;