let eval_with_engine include_paths guistuff grafite_status user_goal
skipped_txt nonskipped_txt st
=
- let module TAPp = GrafiteAstPp in
- let module DTE = DisambiguateTypes.Environment in
let parsed_text_length =
String.length skipped_txt + String.length nonskipped_txt
in
| Cic.Const _ as t ->
PT.Ident (pp_t c t, None)
| Cic.Appl l -> PT.Appl (List.map (aux c) l)
- | Cic.Implicit _ -> PT.Implicit
+ | Cic.Implicit _ -> PT.Implicit `JustOne
| Cic.Lambda (Cic.Name n, s, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
- | Cic.Meta _ -> PT.Implicit
+ | Cic.Meta _ -> PT.Implicit `JustOne
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
| Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
prerr_endline script;
stupid_indenter script
;;
+let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
+ let parsed_text_length = String.length parsed_text in
+ match mac with
+ | TA.Screenshot (_,name) ->
+ let status = script#grafite_status in
+ let _,_,menv,subst,_ = status#obj in
+ let sequent = List.hd menv in
+ let name = Filename.dirname (script#filename) ^ "/" ^ name in
+ guistuff.mathviewer#screenshot status sequent menv subst name;
+ [status, parsed_text], "", parsed_text_length
+ | TA.NCheck (_,t) ->
+ let status = script#grafite_status in
+ let ctx = [] in
+ let m, s, status, t =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status [] [] ctx (parsed_text,parsed_text_length,
+ CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ (* XXX use the metasenv, if possible *)
+ in
+ guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
+ [], "", parsed_text_length
let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
- let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
- let module MDB = LibraryDb in
let module CTC = CicTypeChecker in
- let module CU = CicUniv in
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [({grafite_status with proof_status = No_proof}), parsed_text ],"",
+ [(grafite_status#set_proof_status No_proof), parsed_text ],"",
parsed_text_length
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ ~automation_cache:grafite_status#automation_cache)
proof_status
in
let proof_term =
grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
script ex loc
=
- let module TAPp = GrafiteAstPp in
- let module MD = MultiPassDisambiguator in
- let module ML = MatitaMisc in
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
let grafite_status,macro = lazy_macro context in
eval_macro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+ | GrafiteEngine.NMacro (_loc,macro) ->
+ eval_nmacro include_paths buffer guistuff grafite_status
+ user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+
and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
- let (lexicon_status,st), unparsed_text =
+ let (grafite_status,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))
- (GrafiteTypes.get_estatus grafite_status)
+ grafite_status
in
ast, text
- | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
+ | `Ast (st, text) -> (grafite_status, st), text
in
- let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
let start, stop = HExtlib.loc_of_floc floc in
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
[grafite_status,parsed_text],"",
parsed_text_length
+ | GrafiteParser.LSome (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)))
+ (*when Helm_registry.get_bool "matita.literate" *) ->
+ 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, _)) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let remain_len = String.length unparsed_text - parsed_text_length in
| (statuses,text)::tl ->
(statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
| [] -> [], "", 0)
- | GrafiteParser.LSome (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
let fresh_script_id =
let i = ref 0 in
buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
(* here we need to set the Goal in case we are going to cursor (or to
bottom) and we will face a macro *)
- match self#grafite_status.proof_status with
+ match self#grafite_status#proof_status with
Incomplete_proof p ->
userGoal <-
(try Some (Continuationals.Stack.find_goal p.stack)
let cur_grafite_status =
match history with s::_ -> s | [] -> assert false
in
- LexiconSync.time_travel
- ~present:(GrafiteTypes.get_estatus cur_grafite_status)
- ~past:(GrafiteTypes.get_estatus grafite_status);
+ LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
(* FIXME: this is not correct since there is no undo for
* library_objects.set_default... *)
GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
- LexiconSync.time_travel
- ~present:(GrafiteTypes.get_estatus self#grafite_status)
- ~past:(GrafiteTypes.get_estatus grafite_status)
+ LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
method private reset_buffer =
statements <- [];
HLog.error "The script is too big!\n"
method onGoingProof () =
- match self#grafite_status.proof_status with
+ match self#grafite_status#proof_status with
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
| GrafiteParser.LNone _
| GrafiteParser.LSome (GrafiteAst.Executable _) -> false
in
- try
- is_there_only_comments
- (GrafiteTypes.get_estatus self#grafite_status) self#getFuture
+ try is_there_only_comments self#grafite_status self#getFuture
with
| LexiconEngine.IncludedFileNotCompiled _
| HExtlib.Localized _
projects / helm.git / blobdiff