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 =
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
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 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 =
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
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 =
- 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 =
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 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