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 =
"matita.paste_unicode_as_tex")
~skip_thm_and_qed:true
~skip_initial_lambdas:how_many_lambdas
- 80 GrafiteAst.Declarative "" obj
+ 80 [] obj
else
if true then
(* use cic2grafite *)
Helm_registry.get_bool "matita.paste_unicode_as_tex"
in
ApplyTransformation.procedural_txt_of_cic_term
- ~map_unicode_to_tex 78 cc proof_term
+ ~map_unicode_to_tex 78 [] cc proof_term
in
let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
[],text,parsed_text_length
ProofEngineTypes.Fail _ as exn ->
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
- | TA.Inline (_,style,suri,prefix,flavour) ->
- let str =
+ | TA.Inline (_, suri, params) ->
+ let str = "\n\n" ^
ApplyTransformation.txt_of_inline_macro
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- style ?flavour prefix suri
+ params suri
in
[], str, String.length parsed_text
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 =