(* $Id$ *)
module G = GrafiteAst
-open GrafiteTypes
open Printf
class status baseuri =
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
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
| 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")
| _ -> ""
)
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
(* 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 _ ->
[]