X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8ec91964edff51159a58bb197e2d57f5bdc31aa2;hb=5379335718a93d3e933d9bfdc0dd85f00983bc21;hp=de49a48517ddf2ea75692e51b63546d3dc50d761;hpb=7d47820d03f154a86c966fb72c52f42b6c52176a;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index de49a4851..8ec91964e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -152,10 +152,10 @@ Arg.parse argspec ignore ""
 
 (* A WIDGET TO ENTER CIC TERMS *)
 
-class term_editor ?packing ?width ?height ?changed_callback () =
+class term_editor ?packing ?width ?height ?isnotempty_callback () =
  let input = GEdit.text ~editable:true ?width ?height ?packing () in
  let _ =
-  match changed_callback with
+  match isnotempty_callback with
      None -> ()
    | Some callback ->
       ignore(input#connect#changed (function () -> callback (input#length > 0)))
@@ -530,11 +530,12 @@ let
 =
 (*CSC: ????????????????? *)
  let xml, bodyxml =
-  Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
  in
  let xmlinnertypes =
-  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
-   ~ids_to_inner_types
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
  in
   let input =
    match bodyxml with
@@ -551,6 +552,55 @@ let
     output
 ;;
 
+let
+ save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
+=
+ let name =
+  let struri = UriManager.string_of_uri uri in
+  let idx = (String.rindex struri '/') + 1 in
+   String.sub struri idx (String.length struri - idx)
+ in
+  let path = pathname ^ "/" ^ name in
+  let xml, bodyxml =
+   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+    annobj 
+  in
+  let xmlinnertypes =
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+    ~ask_dtd_to_the_getter:false
+  in
+   (* innertypes *)
+   let innertypesuri = UriManager.innertypesuri_of_uri uri in
+    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+    Getter.register innertypesuri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri innertypesuri) ^ ".xml"
+     ) ;
+    (* constant type / variable / mutual inductive types definition *)
+    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+    Getter.register uri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".xml"
+     ) ;
+    match bodyxml with
+       None -> ()
+     | Some bodyxml' ->
+        (* constant body *)
+        let bodyuri =
+         match UriManager.bodyuri_of_uri uri with
+            None -> assert false
+          | Some bodyuri -> bodyuri
+        in
+         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+         Getter.register bodyuri
+          (Configuration.annotations_url ^
+            Str.replace_first (Str.regexp "^cic:") ""
+             (UriManager.string_of_uri bodyuri) ^ ".xml"
+          )
+;;
+
 
 (* CALLBACKS *)
 
@@ -691,6 +741,15 @@ let mml_of_cic_term metano term =
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
+let pathname_of_annuri uristring =
+ Configuration.annotations_dir ^    
+  Str.replace_first (Str.regexp "^cic:") "" uristring
+;;
+
+let make_dirs dirpath =
+ ignore (Unix.system ("mkdir -p " ^ dirpath))
+;;
+
 let qed () =
  match !ProofEngine.proof with
     None -> assert false
@@ -713,6 +772,12 @@ let qed () =
            ids_to_inner_types
          in
           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
+          !qed_set_sensitive false ;
+          (* let's save the theorem and register it to the getter *) 
+          let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
+          make_dirs pathname ;
+          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
+           pathname ;
           current_cic_infos :=
            Some
             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
@@ -723,12 +788,6 @@ let qed () =
   | _ -> raise OpenConjecturesStillThere
 ;;
 
-(*????
-let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
-let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
-*)
-let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
-
 let save () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   match !ProofEngine.proof with
@@ -742,7 +801,10 @@ let save () =
         Cic2acic.acic_object_of_cic_object currentproof
        in
         let xml, bodyxml =
-         match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
+         match
+          Cic2Xml.print_object uri ~ids_to_inner_sorts
+           ~ask_dtd_to_the_getter:true acurrentproof
+         with
             xml,Some bodyxml -> xml,bodyxml
           | _,None -> assert false
         in
@@ -774,27 +836,33 @@ let load () =
  let output = ((rendering_window ())#output : GMathView.math_view) in
  let notebook = (rendering_window ())#notebook in
   try
-   let uri = UriManager.uri_of_string "cic:/dummy.con" in
-    match CicParser.obj_of_xml prooffiletype (Some prooffile) with
-       Cic.CurrentProof (_,metasenv,bo,ty,_) ->
-        typecheck_loaded_proof metasenv bo ty ;
-        ProofEngine.proof :=
-         Some (uri, metasenv, bo, ty) ;
-        ProofEngine.goal :=
-         (match metasenv with
-             [] -> None
-           | (metano,_,_)::_ -> Some metano
-         ) ;
-        refresh_proof output ;
-        refresh_sequent notebook ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof type loaded from " ^
-            prooffiletype ^ "</h1>") ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof body loaded from " ^
-            prooffile ^ "</h1>") ;
-        !save_set_sensitive true
-     | _ -> assert false
+   match 
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+     "Choose an URI:"
+   with
+      None -> raise NoChoice
+    | Some uri0 ->
+       let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
+        match CicParser.obj_of_xml prooffiletype (Some prooffile) with
+           Cic.CurrentProof (_,metasenv,bo,ty,_) ->
+            typecheck_loaded_proof metasenv bo ty ;
+            ProofEngine.proof :=
+             Some (uri, metasenv, bo, ty) ;
+            ProofEngine.goal :=
+             (match metasenv with
+                 [] -> None
+               | (metano,_,_)::_ -> Some metano
+             ) ;
+            refresh_proof output ;
+            refresh_sequent notebook ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof type loaded from " ^
+                prooffiletype ^ "</h1>") ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof body loaded from " ^
+                prooffile ^ "</h1>") ;
+            !save_set_sensitive true
+         | _ -> assert false
   with
      RefreshSequentException e ->
       output_html outputhtml
@@ -1333,7 +1401,7 @@ let new_proof () =
  let non_empty_type = ref false in
  let window =
   GWindow.window
-   ~width:600 ~modal:true ~title:"New Proof or Definition..."
+   ~width:600 ~modal:true ~title:"New Proof or Definition"
    ~border_width:2 () in
  let vbox = GPack.vbox ~packing:window#add () in
  let hbox =
@@ -1368,7 +1436,7 @@ let new_proof () =
  (* moved here to have visibility of the ok button *)
  let newinputt =
   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
-   ~changed_callback:
+   ~isnotempty_callback:
     (function b ->
       non_empty_type := b ;
       okb#misc#set_sensitive (b && uri_entry#text <> ""))
@@ -1730,7 +1798,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
  let module L = LogicalOperations in
  let module G = Gdome in
   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
-  let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
+  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
    match mmlwidget#get_selection with
@@ -2156,7 +2224,7 @@ end;;
 
 (* Scratch window *)
 
-class scratch_window outputhtml =
+class scratch_window =
  let window =
   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
  let vbox =
@@ -2179,7 +2247,6 @@ class scratch_window outputhtml =
   GMathView.math_view
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
- method outputhtml = outputhtml
  method mmlwidget = mmlwidget
  method show () = window#misc#hide () ; window#show ()
  initializer
@@ -2395,12 +2462,15 @@ end
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
+ let scratch_window = new scratch_window in
  let window =
-  GWindow.window ~title:"MathML viewer" ~border_width:2
+  GWindow.window ~title:"MathML viewer" ~border_width:0
    ~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 handle_box = GBin.handle_box ~border_width:2
+  ~packing:(vbox_for_menu#pack ~padding:0) () in
+ let menubar = GMenu.menu_bar ~packing:handle_box#add () in
  let factory0 = new GMenu.factory menubar in
  let accel_group = factory0#accel_group in
  (* file menu *)
@@ -2409,7 +2479,7 @@ class rendering_window output (notebook : notebook) =
  let export_to_postscript_menu_item =
   begin
    let _ =
-    factory1#add_item "New Proof or Definition" ~key:GdkKeysyms._N
+    factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
      ~callback:new_proof
    in
    let reopen_menu_item =
@@ -2417,10 +2487,10 @@ class rendering_window output (notebook : notebook) =
      ~callback:open_
    in
    let qed_menu_item =
-    factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
+    factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
+    (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
       ~callback:load) ;
    let save_menu_item =
     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
@@ -2432,15 +2502,15 @@ class rendering_window output (notebook : notebook) =
    ignore (!qed_set_sensitive false);
    ignore (factory1#add_separator ()) ;
    let export_to_postscript_menu_item =
-    factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
+    factory1#add_item "Export to PostScript..."
      ~callback:(export_to_postscript output) in
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
+    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
    export_to_postscript_menu_item
   end in
  (* edit menu *)
- let edit_menu = factory0#add_submenu "Edit current proof" in
+ let edit_menu = factory0#add_submenu "Edit Current Proof" 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 =
@@ -2458,6 +2528,13 @@ class rendering_window output (notebook : notebook) =
     focus_menu_item#misc#set_sensitive b
  in
  let _ = !focus_and_proveit_set_sensitive false in
+ (* edit term menu *)
+ let edit_term_menu = factory0#add_submenu "Edit Term" in
+ let factory5 = new GMenu.factory edit_term_menu ~accel_group in
+ let check_menu_item =
+  factory5#add_item "Check Term" ~key:GdkKeysyms._C
+   ~callback:(check scratch_window) in
+ let _ = check_menu_item#misc#set_sensitive false in
  (* search menu *)
  let settings_menu = factory0#add_submenu "Search" in
  let factory4 = new GMenu.factory settings_menu ~accel_group in
@@ -2490,20 +2567,14 @@ class rendering_window output (notebook : notebook) =
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let _ = scrolled_window0#add output#coerce in
  let frame =
-  GBin.frame ~label:"Term input"
+  GBin.frame ~label:"Insert Term"
    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let vbox' =
-  GPack.vbox ~packing:frame#add () in
- let hbox4 =
-  GPack.hbox ~border_width:5 ~packing:(vbox'#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 scrolled_window1 =
   GBin.scrolled_window ~border_width:5
-   ~packing:(vbox'#pack ~expand:true ~padding:0) () in
+   ~packing:frame#add () in
  let inputt =
-  new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in
+  new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
+   ~isnotempty_callback:check_menu_item#misc#set_sensitive in
  let vboxl =
   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
  let _ =
@@ -2518,7 +2589,6 @@ class rendering_window output (notebook : notebook) =
    ~border_width:20
    ~packing:frame#add
    ~show:true () in
- let scratch_window = new scratch_window outputhtml in
 object
  method outputhtml = outputhtml
  method inputt = inputt
@@ -2542,7 +2612,6 @@ object
   set_settings_window settings_window ;
   set_outputhtml outputhtml ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
-  ignore(checkb#connect#clicked (check scratch_window)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
 end;;