From 18ce84578a8aed3b1320ec0b42507f26fc5e3ca4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Apr 2002 12:14:36 +0000
Subject: [PATCH] * Scratch window added * Check command implemented

---
 helm/gTopLevel/gTopLevel.ml | 94 ++++++++++++++++++++++++++++++++++++-
 1 file changed, 93 insertions(+), 1 deletion(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 5726f3d8c..eb02cb07f 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -209,6 +209,28 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
 *)
 ;;
 
+let mml_of_cic_term term =
+ let context =
+  match !ProofEngine.goal with
+     None -> []
+   | Some (_,(context,_)) -> context
+ in
+  let metasenv =
+   match !ProofEngine.proof with
+      None -> []
+    | Some (_,metasenv,_,_) -> metasenv
+  in
+   let sequent_gdome,ids_to_terms,ids_to_father_ids =
+    SequentPp.XmlPp.print_sequent metasenv (context,term)
+   in
+    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 output_html outputhtml msg =
  htmlheader_and_content := !htmlheader_and_content ^ msg ;
  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
@@ -557,6 +579,57 @@ let state rendering_window () =
         print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
 ;;
 
+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
+  let inputlen = inputt#length in
+  let input = inputt#get_chars 0 inputlen ^ "\n" in
+  let curi,metasenv =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (curi,metasenv,_,_) -> curi,metasenv
+  in
+  let ciccontext,names_context =
+   let context =
+    match !ProofEngine.goal with
+       None -> assert false
+     | Some (_,(ctx,_)) -> ctx
+   in
+    ProofEngine.cic_context_of_context context,
+     List.map (function (_,n,_) -> n) context
+  in
+   (* Do something interesting *)
+   let lexbuf = Lexing.from_string input in
+    try
+     while true do
+      (* Execute the actions *)
+      match
+       CicTextualParserContext.main curi names_context CicTextualLexer.token
+        lexbuf
+      with
+         None -> ()
+       | Some expr ->
+          try
+           let ty  = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
+            let mml = mml_of_cic_term ty in
+             scratch_window#show () ;
+             scratch_window#display ~dom:mml
+          with
+           e ->
+            print_endline ("? " ^ CicPp.ppterm expr) ;
+            raise e
+     done
+    with
+       CicTextualParser0.Eof ->
+        inputt#delete_text 0 inputlen ;
+        ignore(oldinputt#insert_text input oldinputt#length)
+     | e ->
+        print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+
 let choose_selection
      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
 =
@@ -702,7 +775,21 @@ object(self)
   ignore(closeb#connect#clicked settings_window#misc#hide)
 end;;
 
-(* Main windows *)
+(* Scratch window *)
+
+class scratch_window () =
+ let window =
+  GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let mmlwidget =
+  GMathView.math_view ~packing:(window#add) ~width:400 ~height:280 () in
+object(self)
+ method display = mmlwidget#load_tree
+ method show = window#show
+ initializer
+  ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
+end;;
+
+(* Main window *)
 
 class rendering_window output proofw (label : GMisc.label) =
  let window =
@@ -745,6 +832,9 @@ class rendering_window output proofw (label : GMisc.label) =
  let openb =
   GButton.button ~label:"Open"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let checkb =
+  GButton.button ~label:"Check"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
    ~packing:(vbox#pack ~padding:5) () in
  let vbox1 =
@@ -791,6 +881,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
 object(self)
  method outputhtml = outputhtml
  method oldinputt = oldinputt
@@ -815,6 +906,7 @@ object(self)
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
   ignore(stateb#connect#clicked (state self)) ;
   ignore(openb#connect#clicked (open_ self)) ;
+  ignore(checkb#connect#clicked (check self scratch_window)) ;
   ignore(exactb#connect#clicked (exact self)) ;
   ignore(applyb#connect#clicked (apply self)) ;
   ignore(elimintrosb#connect#clicked (elimintros self)) ;
-- 
2.39.2