let (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~universe:grafite_status.GrafiteTypes.universe) proof_status
+ ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ proof_status
in
let proof_term =
let irl =
CicNotation2.load_notation ~include_paths:[]
BuildTimeConf.core_notation_script
in
- let grafite_status = GrafiteSync.init baseuri in
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
grafite_status,lexicon_status
in
let read_include_paths file =
let lock = buffer#get_iter_at_mark (`MARK locked_mark) in
let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in
text
-(* THIS SNIPPET AUTOMATICALLY EXPANDS EVERY \TeX MACRO
- if Pcre.pmatch ~pat:"\\\\[a-zA-Z]+" text then
- begin
- buffer#delete ~start:lock ~stop:buffer#end_iter;
- let text =
- Pcre.substitute_substrings
- ~subst:(fun str ->
- let pristine = Pcre.get_substring str 0 in
- let input =
- if pristine.[0] = ' ' then
- String.sub pristine 1 (String.length pristine -1)
- else pristine
- in
- let input =
- if input.[String.length input-1] = ' ' then
- String.sub input 0 (String.length input -1)
- else input
- in
- try
- Glib.Utf8.from_unichar (snd (Virtuals.symbol_of_virtual input))
- with Virtuals.Not_a_virtual -> pristine)
- ~pat:" ?\\\\[a-zA-Z]+ ?" text
- in
- buffer#insert ~iter:lock text;
- text
- end
- else
- text
-*)
+ method expandAllVirtuals =
+ let lock = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in
+ buffer#delete ~start:lock ~stop:buffer#end_iter;
+ let text = Pcre.replace ~pat:":=" ~templ:"\\def" text in
+ let text = Pcre.replace ~pat:"->" ~templ:"\\to" text in
+ let text = Pcre.replace ~pat:"=>" ~templ:"\\Rightarrow" text in
+ let text =
+ Pcre.substitute_substrings
+ ~subst:(fun str ->
+ let pristine = Pcre.get_substring str 0 in
+ let input =
+ if pristine.[0] = ' ' then
+ String.sub pristine 1 (String.length pristine -1)
+ else pristine
+ in
+ let input =
+ if input.[String.length input-1] = ' ' then
+ String.sub input 0 (String.length input -1)
+ else input
+ in
+ let before, after =
+ if input = "\\forall" ||
+ input = "\\lambda" ||
+ input = "\\exists" then "","" else " ", " "
+ in
+ try
+ before ^ Glib.Utf8.from_unichar
+ (snd (Virtuals.symbol_of_virtual input)) ^ after
+ with Virtuals.Not_a_virtual -> pristine)
+ ~pat:" ?\\\\[a-zA-Z]+ ?" text
+ in
+ buffer#insert ~iter:lock text
(** @param rel_offset relative offset from current position of locked_mark *)
method private moveMark rel_offset =