From 0749993af4ee4609f32e5e4f04d40accbbda0e7e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 12 Nov 2002 12:16:27 +0000
Subject: [PATCH] Heavy restyling of the interface.

Open BUG: exportation to PostScript sometimes make the widget core-dump.
---
 helm/gTopLevel/gTopLevel.ml | 267 ++++++++++++++++++++++++------------
 1 file changed, 178 insertions(+), 89 deletions(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c6e8ac763..c4e070193 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -76,6 +76,8 @@ let innertypesfile = "/public/sacerdot/innertypes";;
 let innertypesfile = "/public/sacerdot/innertypes";;
 let constanttypefile = "/public/sacerdot/constanttype";;
 
+let empty_id_to_uris = ([],function _ -> None);;
+
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -85,7 +87,7 @@ let current_cic_infos = ref None;;
 let current_goal_infos = ref None;;
 let current_scratch_infos = ref None;;
 
-let id_to_uris = ref ([],function _ -> None);;
+let id_to_uris = ref empty_id_to_uris;;
 
 let check_term = ref (fun _ _ _ -> assert false);;
 
@@ -100,7 +102,18 @@ let set_rendering_window,rendering_window =
      | Some rw -> rw
   )
 ;;
-ref None;;
+
+exception SettingsWindowsNotInitialized;;
+
+let set_settings_window,settings_window =
+ let settings_window_ref = ref None in
+  (function rw -> settings_window_ref := Some rw),
+  (function () ->
+    match !settings_window_ref with
+       None -> raise SettingsWindowsNotInitialized
+     | Some rw -> rw
+  )
+;;
 
 (* COMMAND LINE OPTIONS *)
 
@@ -116,7 +129,7 @@ Arg.parse argspec ignore ""
 
 (* MISC FUNCTIONS *)
 
-let cic_textual_parser_uri_of_uri uri' =
+let cic_textual_parser_uri_of_string uri' =
  (* Constant *)
  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
@@ -138,17 +151,33 @@ let cic_textual_parser_uri_of_uri uri' =
    )
 ;;
 
-
-let term_of_uri uri =
+let term_of_cic_textual_parser_uri uri =
  let module C = Cic in
  let module CTP = CicTextualParser0 in
-  match (cic_textual_parser_uri_of_uri uri) with
+  match uri with
      CTP.ConUri uri -> C.Const (uri,[])
    | CTP.VarUri uri -> C.Var (uri,[])
    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 ;;
 
+let string_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+  let uri' =
+   match uri with
+      CTP.ConUri uri -> UriManager.string_of_uri uri
+    | CTP.VarUri uri -> UriManager.string_of_uri uri
+    | CTP.IndTyUri (uri,tyno) ->
+       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
+    | CTP.IndConUri (uri,tyno,consno) ->
+       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
+        string_of_int consno
+  in
+   (* 4 = String.length "cic:" *)
+   String.sub uri' 4 (String.length uri' - 4)
+;;
+
 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 
 exception NoChoice;;
@@ -178,7 +207,11 @@ let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris =
   choice := Some combo#entry#text ;
   window#destroy ()
  in
- let check_callback () = !check_term [] [] (term_of_uri combo#entry#text) in
+ let check_callback () =
+   !check_term [] []
+    (term_of_cic_textual_parser_uri
+     (cic_textual_parser_uri_of_string combo#entry#text))
+ in
   ignore (window#connect#destroy GMain.Main.quit) ;
   ignore (cancelb#connect#clicked window#destroy) ;
   ignore (okb#connect#clicked ok_callback) ;
@@ -247,7 +280,7 @@ let locate_one_id id =
       with
        NoChoice -> uris
   in
-   List.map cic_textual_parser_uri_of_uri uris'
+   List.map cic_textual_parser_uri_of_string uris'
 ;;
 
 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
@@ -1103,6 +1136,28 @@ let load () =
        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let edit_aliases () =
+ let inputt = ((rendering_window ())#inputt : GEdit.text) in
+ let dom,resolve_id = !id_to_uris in
+  let inputlen = inputt#length in
+   inputt#delete_text 0 inputlen ;
+   let _ =
+    inputt#insert_text ~pos:0
+     (String.concat "\n"
+       (List.map
+         (function v ->
+           let uri =
+            match resolve_id v with
+               None -> assert false
+             | Some uri -> uri
+           in
+            "alias " ^ v ^ " " ^
+              (string_of_cic_textual_parser_uri uri)
+         ) dom))
+   in
+    id_to_uris := empty_id_to_uris
+;;
+
 let proveit () =
  let module L = LogicalOperations in
  let module G = Gdome in
@@ -1217,7 +1272,6 @@ exception NotADefinition;;
 
 let open_ () =
  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 notebook = (rendering_window ())#notebook in
@@ -1239,8 +1293,7 @@ let open_ () =
       ProofEngine.goal := None ;
       refresh_sequent notebook ;
       refresh_proof output ;
-      inputt#delete_text 0 inputlen ;
-      ignore(oldinputt#insert_text input oldinputt#length)
+      inputt#delete_text 0 inputlen
    with
       RefreshSequentException e ->
        output_html outputhtml
@@ -1257,7 +1310,6 @@ let open_ () =
 
 let state () =
  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 notebook = (rendering_window ())#notebook in
@@ -1287,8 +1339,7 @@ let state () =
      done
     with
        CicTextualParser0.Eof ->
-        inputt#delete_text 0 inputlen ;
-        ignore(oldinputt#insert_text input oldinputt#length)
+        inputt#delete_text 0 inputlen
      | RefreshSequentException e ->
         output_html outputhtml
          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
@@ -1444,7 +1495,11 @@ let searchPattern () =
              | uri::tl ->
                 let tl',exc = filter_out tl in
                  try
-                  if ProofEngine.can_apply (term_of_uri uri) then
+                  if
+                   ProofEngine.can_apply
+                    (term_of_cic_textual_parser_uri
+                     (cic_textual_parser_uri_of_string uri))
+                  then
                    uri::tl',exc
                   else
                    tl',exc
@@ -1507,12 +1562,20 @@ let choose_selection
 
 (* Stuff for the widget settings *)
 
-let export_to_postscript (output : GMathView.math_view) () =
- output#export_to_postscript ~filename:"output.ps" ();
+let export_to_postscript (output : GMathView.math_view) =
+ let lastdir = ref (Unix.getcwd ()) in
+  function () ->
+   match
+    GToolbox.select_file ~title:"Export to PostScript"
+     ~dir:lastdir ~filename:"screenshot.ps" ()
+   with
+      None -> ()
+    | Some filename ->
+       output#export_to_postscript ~filename:filename ();
 ;;
 
 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
- button_set_kerning button_set_transparency button_export_to_postscript
+ button_set_kerning button_set_transparency export_to_postscript_menu_item
  button_t1 ()
 =
  let is_set = button_t1#active in
@@ -1523,14 +1586,14 @@ let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
     button_set_anti_aliasing#misc#set_sensitive true ;
     button_set_kerning#misc#set_sensitive true ;
     button_set_transparency#misc#set_sensitive true ;
-    button_export_to_postscript#misc#set_sensitive true ;
+    export_to_postscript_menu_item#misc#set_sensitive true ;
    end
   else
    begin
     button_set_anti_aliasing#misc#set_sensitive false ;
     button_set_kerning#misc#set_sensitive false ;
     button_set_transparency#misc#set_sensitive false ;
-    button_export_to_postscript#misc#set_sensitive false ;
+    export_to_postscript_menu_item#misc#set_sensitive false ;
    end
 ;;
 
@@ -1555,7 +1618,7 @@ let set_log_verbosity output log_verbosity_spinb () =
 ;;
 
 class settings_window (output : GMathView.math_view) sw
- button_export_to_postscript selection_changed_callback
+ export_to_postscript_menu_item selection_changed_callback
 =
  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
  let vbox =
@@ -1612,7 +1675,7 @@ object(self)
   (* Signals connection *)
   ignore(button_t1#connect#clicked
    (activate_t1 output button_set_anti_aliasing button_set_kerning
-    button_set_transparency button_export_to_postscript button_t1)) ;
+    button_set_transparency export_to_postscript_menu_item button_t1)) ;
   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
   ignore(button_set_anti_aliasing#connect#toggled
    (set_anti_aliasing output button_set_anti_aliasing));
@@ -1701,11 +1764,11 @@ class page () =
  let cutb =
   GButton.button ~label:"Cut"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let changeb =
-  GButton.button ~label:"Change"
-   ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
  let hbox4 =
   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let changeb =
+  GButton.button ~label:"Change"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let letinb =
   GButton.button ~label:"Let ... In"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1727,14 +1790,14 @@ class page () =
  let reflexivityb =
   GButton.button ~label:"Reflexivity"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox5 =
+  GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
  let symmetryb =
   GButton.button ~label:"Symmetry"
-   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
  let transitivityb =
   GButton.button ~label:"Transitivity"
-   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
- let hbox5 =
-  GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+   ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
  let leftb =
   GButton.button ~label:"Left"
    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1817,48 +1880,75 @@ end
 
 (* Main window *)
 
-class rendering_window output (notebook : notebook) (label : GMisc.label) =
+class rendering_window output (notebook : notebook) =
  let window =
-  GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+  GWindow.window ~title:"MathML viewer" ~border_width:2
+   ~allow_shrink:false () in
+ let vbox_for_menu = GPack.vbox ~packing:window#add () in
+ (* menus *)
+ let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
+ let factory0 = new GMenu.factory menubar in
+ let accel_group = factory0#accel_group in
+ (* file menu *)
+ let file_menu = factory0#add_submenu "File" in
+ let factory1 = new GMenu.factory file_menu ~accel_group in
+ 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) ;
+   ignore (factory1#add_separator ()) ;
+   let export_to_postscript_menu_item =
+    factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
+     ~callback:(export_to_postscript output) in
+   ignore (factory1#add_separator ()) ;
+   ignore
+    (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
+   export_to_postscript_menu_item
+  end in
+ (* edit menu *)
+ let edit_menu = factory0#add_submenu "Edit" in
+ let factory2 = new GMenu.factory edit_menu ~accel_group in
+ let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
+ let proveit_menu_item =
+  factory2#add_item "Prove It" ~key:GdkKeysyms._I
+   ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
+ in
+ let focus_menu_item =
+  factory2#add_item "Focus" ~key:GdkKeysyms._F
+   ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
+ in
+ let _ =
+  focus_and_proveit_set_sensitive :=
+   function b ->
+    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
+ let factory3 = new GMenu.factory settings_menu ~accel_group in
+ let _ =
+  factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
+   ~callback:edit_aliases in
+ let _ = factory3#add_separator () in
+ let _ =
+  factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
+   ~callback:(function _ -> (settings_window ())#show ()) in
+ (* accel group *)
+ let _ = window#add_accel_group accel_group in
+ (* end of menus *)
  let hbox0 =
-  GPack.hbox ~packing:window#add () in
+  GPack.hbox
+   ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
  let vbox =
-  GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
- let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
+  GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let _ = scrolled_window0#add output#coerce in
- let hbox1 =
-  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let settingsb =
-  GButton.button ~label:"Settings"
-   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let button_export_to_postscript =
-  GButton.button ~label:"export_to_postscript"
-  ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let qedb =
-  GButton.button ~label:"Qed"
-   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let saveb =
-  GButton.button ~label:"Save"
-   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let loadb =
-  GButton.button ~label:"Load"
-   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let closeb =
-  GButton.button ~label:"Close"
-   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
- let hbox2 =
-  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
- let proveitb =
-  GButton.button ~label:"Prove It"
-   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
- let focusb =
-  GButton.button ~label:"Focus"
-   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
- let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
-   ~packing:(vbox#pack ~padding:5) () in
  let hbox4 =
   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let stateb =
@@ -1876,44 +1966,44 @@ class rendering_window output (notebook : notebook) (label : GMisc.label) =
  let searchpatternb =
   GButton.button ~label:"SearchPattern"
    ~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 scrolled_window1 =
+  GBin.scrolled_window ~border_width:10
+   ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let inputt = GEdit.text ~editable:true ~width:400 ~height:100
+   ~packing:scrolled_window1#add () in
  let vboxl =
-  GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+  GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
  let _ =
-  vboxl#pack ~expand:false ~fill:false ~padding:5 notebook#notebook#coerce in
+  vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
  let outputhtml =
   GHtml.xmhtml
    ~source:"<html><body bgColor=\"white\"></body></html>"
-   ~width:400 ~height: 200
-   ~packing:(vboxl#pack ~expand:false ~fill:false ~padding:5)
+   ~width:400 ~height: 100
+   ~border_width:20
+   ~packing:(vboxl#pack ~expand:true ~padding:5)
    ~show:true () in
  let scratch_window = new scratch_window outputhtml in
 object
  method outputhtml = outputhtml
- method oldinputt = oldinputt
  method inputt = inputt
  method output = (output : GMathView.math_view)
  method notebook = notebook
  method show = window#show
  initializer
   notebook#set_empty_page ;
-  button_export_to_postscript#misc#set_sensitive false ;
+  export_to_postscript_menu_item#misc#set_sensitive false ;
   check_term := (check_term_in_scratch scratch_window) ;
 
   (* signal handlers here *)
   ignore(output#connect#selection_changed
-   (function elem -> notebook#proofw#unload ; choose_selection output elem)) ;
-  ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
+   (function elem ->
+     notebook#proofw#unload ;
+     choose_selection output elem ;
+     !focus_and_proveit_set_sensitive true
+   )) ;
   let settings_window = new settings_window output scrolled_window0
-   button_export_to_postscript (choose_selection output) in
-  ignore(settingsb#connect#clicked settings_window#show) ;
-  ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
-  ignore(qedb#connect#clicked qed) ;
-  ignore(saveb#connect#clicked save) ;
-  ignore(loadb#connect#clicked load) ;
-  ignore(proveitb#connect#clicked proveit) ;
-  ignore(focusb#connect#clicked focus) ;
+   export_to_postscript_menu_item (choose_selection output) in
+  set_settings_window settings_window ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
   ignore(stateb#connect#clicked state) ;
   ignore(openb#connect#clicked open_) ;
@@ -1930,17 +2020,16 @@ let initialize_everything () =
  let module U = Unix in
   let output = GMathView.math_view ~width:350 ~height:280 () in
   let notebook = new notebook in
-  let label = GMisc.label ~text:"gTopLevel" () in
-    let rendering_window' = new rendering_window output notebook label in
-     set_rendering_window rendering_window' ;
-     rendering_window'#show () ;
-     GMain.Main.main ()
+   let rendering_window' = new rendering_window output notebook in
+    set_rendering_window rendering_window' ;
+    rendering_window'#show () ;
+    GMain.Main.main ()
 ;;
 
 let _ =
  if !usedb then
-(* Mqint.init "dbname=helm_mowgli" ; *)
- Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
+ Mqint.init "dbname=helm_mowgli" ; 
+(* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  if !usedb then Mqint.close ();
-- 
2.39.2