matita gtk3: some bugs fixed

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

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index cfd8c107a49e57784eddd46e6c1ce600cf5e32ca..6b4c6655b03a9d1ddc4769b10a80e4ed05295d0d 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -26,7 +26,6 @@
 (* $Id$ *)
 
 module G = GrafiteAst
-open GrafiteTypes
 open Printf
 
 class status baseuri =
@@ -51,7 +50,7 @@ let first_line = ref true ;;
 let cases_or_induction_context stack =
     match stack with
      [] -> false
-    | (g,t,k,tag,p)::tl -> try
+    | (_g,_t,_k,_tag,p)::_tl -> try
                             let s = List.assoc "context" p in
                             s = "cases" || s = "induction"
                            with
@@ -61,10 +60,10 @@ let cases_or_induction_context stack =
 let has_focused_goal stack =
     match stack with
      [] -> false
-    | (g,t,k,tag,p)::tl -> (List.length g) > 0
+    | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
 ;;
 
-let get_indentation status statement =
+let get_indentation status _statement =
   let base_ind =
     match status#stack with
       [] -> 0
@@ -105,7 +104,7 @@ let write_ast_to_file status fname statement =
                 | G.NObj (_,obj,_) ->
                         (
                         match obj with
-                            Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+                            NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
                                    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
                         |   _ -> ""
                         )
@@ -123,9 +122,9 @@ let write_ast_to_file status fname statement =
           else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
         in
         let out_channel =
-          Stdlib.open_out_gen flaglist 0o0644 fname in
-        let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
-        let _ = Stdlib.close_out out_channel in
+          open_out_gen flaglist 0o0644 fname in
+        let _ = output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
+        let _ = close_out out_channel in
         str
       )
     else
@@ -252,17 +251,17 @@ let baseuri_of_script ~include_paths fname =
 
 (* given a path to a ma file inside the include_paths, returns the
    new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
-  try
-    let root, _buri, _fname, _tgt =
-      Librarian.baseuri_of_script ~include_paths:[] file in
-    let includes =
-      try
-        Str.split (Str.regexp " ")
-          (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
-      with Not_found -> []
-    in
-    let rc = root :: includes in
+let read_include_paths ~include_paths:_ file =
+ try 
+   let root, _buri, _fname, _tgt = 
+     Librarian.baseuri_of_script ~include_paths:[] file in 
+   let includes =
+    try
+     Str.split (Str.regexp " ") 
+      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+    with Not_found -> []
+   in
+   let rc = root :: includes in
     List.iter (HLog.debug) rc; rc
   with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
     []