match cont with
| None -> asserted, true, status
| Some (asserted,ast) ->
+ (* pp_ast_statement status ast; *)
cb status ast;
let status =
eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
in
asserted, false, status
with exn when not matita_debug ->
+ prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status
if List.mem fname compiling then raise (CircularDependency fname);
let compiling = fname::compiling in
let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let matita_debug = true in
let root,baseuri,fname,_tgt =
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
(Filename.dirname
(Http_getter.filename ~local:true ~writable:true (baseuri ^
"foo.con")));
+ prerr_endline ("trying to compile " ^ fname);
let buf =
GrafiteParser.parsable_statement status
(Ulexing.from_utf8_channel (open_in fname))
in
let asserted, status =
eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+ prerr_endline ("end compile of " ^ fname);
let elapsed = Unix.time () -. time in
(if Helm_registry.get_bool "matita.moo" then begin
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times fname true big_bang big_bang_u big_bang_s;
- (* XXX: update script -- currently to stdout *)
+ prerr_endline ("now generating disambiguated script for " ^ fname);
let origbuf = Ulexing.from_utf8_channel (open_in fname) in
let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
Printf.fprintf outch "%s" !outstr;
+ prerr_endline ("returning after compilation of " ^ fname);
asserted
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel
end
;;
+let eos status s =
+ let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" in
+ let rec is_there_only_comments status s =
+ if Pcre.pmatch ~rex:only_dust_RE s then raise End_of_file;
+ let strm =
+ GrafiteParser.parsable_statement status
+ (Ulexing.from_utf8_string s) in
+ match GrafiteParser.parse_statement status strm with
+ | GrafiteAst.Comment (loc,_) ->
+ let _,parsed_text_length = HExtlib.utf8_parsed_text s loc in
+ (* CSC: why +1 in the following lines ???? *)
+ let parsed_text_length = parsed_text_length + 1 in
+ let remain_len = String.length s - parsed_text_length in
+ let next = String.sub s parsed_text_length remain_len in
+ is_there_only_comments status next
+ | GrafiteAst.Executable _ -> false
+ in
+ try is_there_only_comments status s
+ with
+ | NCicLibrary.IncludedFileNotCompiled _
+ | HExtlib.Localized _
+ | CicNotationParser.Parse_error _ -> false
+ | End_of_file -> true
+ | Invalid_argument "Array.make" -> false
+;;
+
+
let assert_ng ~include_paths ?outch mapath =
snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
?outch mapath)