added support for directory browsing in cicBrowser

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 922cc7b9a80bb069cac15a1eca1d4cbbc8d181c0..4d3137d55e74e56bea5de9e36979a7993b2a2e74 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -287,21 +287,22 @@ let save_object_to_disk uri obj =
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
   let bodyuri = UriManager.bodyuri_of_uri uri in
   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri innertypesuri) ^ ".xml" in
+        (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
   let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in
   let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
-        (UriManager.string_of_uri uri) ^ ".xml" in
+        (UriManager.string_of_uri uri) ^ ".xml.gz" in
   let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in
   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
-        (UriManager.string_of_uri uri) ^ ".body.xml" in
+        (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
   let xmlbodypath = !(Lazy.force basedir) ^ "/" ^  xmlbodyfilename in
   let path_scheme_of path = "file://" ^ path in
   MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]);
    (* now write to disk *)
     ensure_path_exists innertypespath;
-    Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
+    Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
     ensure_path_exists xmlpath;
-    Xml.pp ~quiet:true xml (Some xmlpath) ;
+    Xml.pp ~gzip:true xml (Some xmlpath) ;
+    
    (* now register to the getter *)
     Http_getter.register' innertypesuri (path_scheme_of innertypespath); 
     Http_getter.register' uri (path_scheme_of xmlpath);
@@ -310,7 +311,7 @@ let save_object_to_disk uri obj =
        None,None -> ()
      | Some bodyxml,Some bodyuri->
          ensure_path_exists xmlbodypath;
-         Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
+         Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
          Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
      | _-> assert false) 
 
@@ -555,10 +556,14 @@ class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
           Tactics.replace ~what:(self#disambiguate what)
             ~with_what:(self#disambiguate with_what)
       | TacticAst.Auto -> Tactics.auto_new ~dbd
+      | TacticAst.Change (what, with_what, _) ->
+          let what = self#disambiguate what in
+          let with_what = self#disambiguate with_what in
+          Tactics.change ~what ~with_what
     (*
       (* TODO Zack a lot more of tactics to be implemented here ... *)
-      | TacticAst.Change of 'term * 'term * 'ident option
       | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+      | TacticAst.Change of 'term * 'term * 'ident option
       | TacticAst.Decompose of 'ident * 'ident list
       | TacticAst.Discriminate of 'ident
       | TacticAst.Fold of reduction_kind * 'term