X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;h=3757b177f1706dc3fc290c8f402a20af3a51dbe0;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=48ff2d360dc5394ba01ee090540fa899c3807baa;hpb=dee464f8cd331524663167659d1fad01e558d4e1;p=helm.git diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 48ff2d360..3757b177f 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -135,7 +135,7 @@ let baseuri_of_script ~include_paths fname = let rec get_ast status ~compiling ~asserted ~include_paths strm = match GrafiteParser.parse_statement status strm with (GrafiteAst.Executable - (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd + (loc,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> let already_included = NCicLibrary.get_transitively_included status in let asserted,_ = @@ -147,31 +147,42 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm = and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in - let rec loop asserted status = - let asserted,stop,status = + let rec loop asserted status str = + let asserted,stop,status,str = try let cont = try Some (get_ast status ~compiling ~asserted ~include_paths str) with End_of_file -> None in match cont with - | None -> asserted, true, status + | None -> asserted, true, status, str | Some (asserted,ast) -> cb status ast; let status = eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in - asserted, false, status + let str = + match ast with + (GrafiteAst.Executable + (_,GrafiteAst.NCommand + (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) -> + GrafiteParser.parsable_statement status + (GrafiteParser.strm_of_parsable str) + | _ -> str + in + asserted, false, status, str 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 stop then asserted,status else loop asserted status str in - loop asserted status + loop asserted status str and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = 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; @@ -211,6 +222,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = (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)) @@ -221,6 +233,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid 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) @@ -237,7 +250,6 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = 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 *) let origbuf = Ulexing.from_utf8_channel (open_in fname) in let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in let outstr = ref "" in @@ -266,8 +278,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid let ngtime_of baseuri = let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in - prerr_endline ("uid = " ^ uid); - prerr_endline ("ngpath = " ^ ngpath); + (* prerr_endline ("uid = " ^ uid); + prerr_endline ("ngpath = " ^ ngpath); *) try Some (Unix.stat ngpath).Unix.st_mtime with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in @@ -299,7 +311,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid asserted, children_bad || matime > ngtime | None -> asserted,true in - prerr_endline ("asserted = " ^ (String.concat "," asserted)); + (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *) if not to_be_compiled then fullmapath::asserted,false else if List.mem baseuri already_included then @@ -311,13 +323,40 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid | None -> open_out (fullmapath ^ ".mad"), true | Some c -> c, false in - prerr_endline ("compiling " ^ fullmapath); + (* prerr_endline ("compiling " ^ fullmapath); *) let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in if is_file_ch then close_out outch; fullmapath::asserted,true 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)