Rendering of InductiveDefinitions, Variables and Axioms implemented.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3b6eaff25cc00309222d5f4b6cf18df1f2460bcc..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 =
@@ -739,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)
 ;;
 
 (*
@@ -2026,20 +2030,42 @@ 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 ~skip_switch_page_event:skip =
-  List.iter (function _ -> notebook#remove_page 0) !pages ;
+  if empty then
+   notebook#remove_page 0 (* let's remove the empty page *)
+  else
+   List.iter (function _ -> notebook#remove_page 0) !pages ;
   pages := [] ;
   skip_switch_page_event <- skip
  method set_current_page ~may_skip_switch_page_event n =
@@ -2048,7 +2074,12 @@ object(self)
     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