X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FmatitaScript.ml;h=3a73d6ce6d2d38cbb2425e04c9ad670ea8f59112;hb=5e924927db28c0a5bbbaa4e56515d9afe0b1360f;hp=b8a72a4d24e53dc0fc190ec388d6fc17c11e9141;hpb=30bbfa78612ca1ad0c131a75d7075cfd35bebbe1;p=helm.git diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b8a72a4d2..3a73d6ce6 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -99,27 +99,6 @@ let eval_with_engine include_paths guistuff grafite_status user_goal 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 x = - match f x with - GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand - (_,GrafiteAst.Include (_,_,mafilename)))) as cmd -> - 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 - if MatitacLib.Make.make root [tgt] then - cmd - else raise (Failure ("Compiling: " ^ tgt)) - | cmd -> cmd -;; - 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 = @@ -139,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,12 +193,11 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff 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 grafite_status) - (Ulexing.from_utf8_string text) - in - ast, text + let grammar = CicNotationParser.level2_ast_grammar grafite_status in + let strm = + Grammar.parsable grammar (Obj.magic(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 = @@ -227,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 @@ -276,16 +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 LexiconTypes.status in + let empty_lstatus = new GrafiteDisambiguate.status in (match current with Some current -> 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 = empty_lstatus in - let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#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 = @@ -686,18 +665,18 @@ object (self) method eos = let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - match - GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s) - with - | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> + let grammar = CicNotationParser.level2_ast_grammar lexicon_status in + let strm = + Grammar.parsable grammar (Obj.magic(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