The scratch window is now based on the sequent_viewer widget.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 5b0f3d6e78dcef6852bec20984c5219b4bbe38d2..c02711dd35afaa575e16dfe4ef20fe856381b696 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -73,8 +73,6 @@ let postgresqlconnectionstring =
 
 let htmlheader_and_content = ref htmlheader;;
 
-let current_scratch_infos = ref None
-
 let check_term = ref (fun _ _ _ -> assert false);;
 
 exception RenderingWindowsNotInitialized;;
@@ -191,7 +189,7 @@ let check_window outputhtml uris =
      in
       lazy 
        (let mmlwidget =
-         GMathViewAux.single_selection_math_view
+         TermViewer.sequent_viewer
           ~packing:scrolled_window#add ~width:400 ~height:280 () in
         let expr =
          let term =
@@ -201,11 +199,7 @@ let check_window outputhtml uris =
           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
         in
          try
-          let mml,scratch_infos =
-           ApplyStylesheets.mml_of_cic_term 111 expr
-          in
-           current_scratch_infos := Some scratch_infos ;
-           mmlwidget#load_doc ~dom:mml
+          mmlwidget#load_sequent [] (111,[],expr)
          with
           e ->
            output_html outputhtml
@@ -665,10 +659,8 @@ with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ "
 module InvokeTacticsCallbacks =
  struct
   let sequent_viewer () = (rendering_window ())#notebook#proofw
-  let term_editor () = ((rendering_window ())#inputt : TermEditor.term_editor)
-  let get_current_scratch_infos () = !current_scratch_infos
-  let set_current_scratch_infos scratch_infos =
-   current_scratch_infos := scratch_infos
+  let term_editor () = (rendering_window ())#inputt
+  let scratch_window () = (rendering_window ())#scratch_window
 
   let refresh_proof () =
    let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
@@ -1569,12 +1561,12 @@ let new_proof () =
 let check_term_in_scratch scratch_window metasenv context expr = 
  try
   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
-  let mml,scratch_infos =
-   ApplyStylesheets.mml_of_cic_term 111 (Cic.Cast (expr,ty))
-  in
-    current_scratch_infos := Some scratch_infos ;
-    scratch_window#show () ;
-    scratch_window#mmlwidget#load_doc ~dom:mml
+  let expr = Cic.Cast (expr,ty) in
+   scratch_window#show () ;
+   scratch_window#set_term expr ;
+   scratch_window#set_context context ;
+   scratch_window#set_metasenv metasenv ;
+   scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr)
  with
   e ->
    print_endline ("? " ^ CicPp.ppterm expr) ;
@@ -2362,18 +2354,28 @@ class scratch_window =
  let scrolled_window =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
- let mmlwidget =
-  GMathViewAux.multi_selection_math_view
+ let sequent_viewer =
+  TermViewer.sequent_viewer
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
- method mmlwidget = mmlwidget
+ val mutable term = Cic.Rel 1                 (* dummy value *)
+ val mutable context = ([] : Cic.context)     (* dummy value *)
+ val mutable metasenv = ([] : Cic.metasenv)   (* dummy value *)
+ method sequent_viewer = sequent_viewer
  method show () = window#misc#hide () ; window#show ()
+ method term = term
+ method set_term t = term <- t
+ method context = context
+ method set_context t = context <- t
+ method metasenv = metasenv
+ method set_metasenv t = metasenv <- t
  initializer
-  ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
+  ignore
+   (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer));
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
-  ignore(whdb#connect#clicked (InvokeTactics'.whd_in_scratch self)) ;
-  ignore(reduceb#connect#clicked (InvokeTactics'.reduce_in_scratch self)) ;
-  ignore(simplb#connect#clicked (InvokeTactics'.simpl_in_scratch self))
+  ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ;
+  ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ;
+  ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch)
 end;;
 
 let open_contextual_menu_for_selected_terms mmlwidget infos =
@@ -2815,6 +2817,7 @@ object
  method outputhtml = outputhtml
  method inputt = inputt
  method output = (output : TermViewer.proof_viewer)
+ method scratch_window = scratch_window
  method notebook = notebook
  method show = window#show
  initializer