Bug fixed: conjectures were printed in the wrong order.

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 22bb994550a76780df5b9787e9fb091654e60447..58e785dec3ef37c5ff6cf8dfc4dad4d2819b3ba5 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -485,9 +485,11 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr =
    in
     aux dom' list_of_uris
   in
-   output_html (outputhtml ())
-    ("<h1>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 ())
+      ("<h1>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 =
@@ -687,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
@@ -702,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
@@ -729,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)
 ;;
 
 (*
@@ -2016,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