X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=b84180037b5ad92716267ce1022b19cc74e72550;hb=4e7e01cd771c07b3605ba54d3853ac34a02cb86d;hp=6221e4901c53ec37937d6e6488d7f82bea231937;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 6221e4901..b84180037 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -80,7 +80,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let text = skipped_txt ^ nonskipped_txt in let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in let enriched_history_fragment = - MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool "matita.do_heavy_checks") grafite_status (text,prefix_len,st) in @@ -92,38 +92,13 @@ let eval_with_engine include_paths guistuff grafite_status user_goal match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" | Some (k,value) -> - let newtxt = LexiconAstPp.pp_alias value in + let newtxt = GrafiteAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in res,"",parsed_text_length ;; -(* this function calls the parser in a way that it does not perform inclusions, - * so that we can ensure the inclusion is performed after the included file - * is compiled (if needed). matitac does not need that, since it compiles files - * in the good order, here files may be compiled on demand. *) -let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = - try - f ~never_include:true ~include_paths x - with - | GrafiteParser.NoInclusionPerformed mafilename -> - let root, buri, _, tgt = - try Librarian.baseuri_of_script ~include_paths mafilename - with Librarian.NoRootFor _ -> - HLog.error ("The included file '"^mafilename^"' has no root file,"); - HLog.error "please create it."; - raise (Failure ("No root file for "^mafilename)) - in - let b = MatitacLib.Make.make root [tgt] in - if b then - try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ -> - raise - (Failure ("Including: "^tgt^ - "\nNothing to do... did you run matitadep?")) - else raise (Failure ("Compiling: " ^ tgt)) -;; - let pp_eager_statement_ast = GrafiteAstPp.pp_statement let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = @@ -143,12 +118,17 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let status = script#grafite_status in let _,_,menv,subst,_ = status#obj in let ctx = - try let _,(_,ctx,_) = List.hd menv in ctx - with Failure "hd" -> [] - in + match Continuationals.Stack.head_goals status#stack with + [] -> [] + | g::tl -> + if tl <> [] then + HLog.warn + "Many goals focused. Using the context of the first one\n"; + let _, ctx, _ = NCicUtils.lookup_meta g menv in + ctx in let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm - None status ctx menv subst (parsed_text,parsed_text_length, + status None ctx menv subst (parsed_text,parsed_text_length, NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in @@ -209,17 +189,16 @@ script ex loc and eval_statement include_paths (buffer : GText.buffer) guistuff grafite_status user_goal script statement = - let (grafite_status,st), unparsed_text = + let st,unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - let ast = - wrap_with_make include_paths - (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) - grafite_status - in - ast, text - | `Ast (st, text) -> (grafite_status, st), text + let strm = + GrafiteParser.parsable_statement grafite_status + (Ulexing.from_utf8_string text) in + let ast = MatitaEngine.get_ast grafite_status include_paths strm in + ast, text + | `Ast (st, text) -> st, text in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in @@ -231,20 +210,16 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff txt,nonskipped_txt,skipped_txt,len in match st with - | GrafiteParser.LNone loc -> - let parsed_text, _, _, parsed_text_length = text_of_loc loc in - [grafite_status,parsed_text],"", - parsed_text_length - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> + | GrafiteAst.Executable (loc, ex) -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff grafite_status user_goal unparsed_text skipped nonskipped script ex loc - | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> + | GrafiteAst.Comment (loc, _) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in @@ -280,20 +255,16 @@ class script ~(source_view: GSourceView2.source_view) let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses current baseuri = - let empty_lstatus = new LexiconEngine.status in + let empty_lstatus = new GrafiteDisambiguate.status in (match current with Some current -> - LexiconSync.time_travel ~present:current ~past:empty_lstatus; NCicLibrary.time_travel - ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus); + ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db); (* CSC: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); - let lexicon_status = - CicNotation2.load_notation ~include_paths:[] empty_lstatus - BuildTimeConf.core_notation_script - in - let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in + let lexicon_status = empty_lstatus in + let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in grafite_status in let read_include_paths file = @@ -422,13 +393,7 @@ object (self) bottom) and we will face a macro *) userGoal <- None - method private _retract offset grafite_status new_statements - new_history - = - let cur_grafite_status = - match history with s::_ -> s | [] -> assert false - in - LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status; + method private _retract offset grafite_status new_statements new_history = NCicLibrary.time_travel grafite_status; statements <- new_statements; history <- new_history; @@ -700,24 +665,22 @@ object (self) method eos = let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let lexicon_status,st = - GrafiteParser.parse_statement (Ulexing.from_utf8_string s) - ~include_paths:self#include_paths lexicon_status - in - match st with - | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> + let strm = + GrafiteParser.parsable_statement lexicon_status + (Ulexing.from_utf8_string s)in + match GrafiteParser.parse_statement lexicon_status strm with + | GrafiteAst.Comment (loc,_) -> let _,parsed_text_length = MatitaGtkMisc.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 lexicon_status next - | GrafiteParser.LNone _ - | GrafiteParser.LSome (GrafiteAst.Executable _) -> false + | GrafiteAst.Executable _ -> false in try is_there_only_comments self#grafite_status self#getFuture with - | LexiconEngine.IncludedFileNotCompiled _ + | NCicLibrary.IncludedFileNotCompiled _ | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true