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
status None ctx menv subst (parsed_text,parsed_text_length,
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
- let ast = MatitaEngine.toplevel grafite_status include_paths text in
+ 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
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
+ 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 ???? *)