in
guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
[status, parsed_text], "", parsed_text_length
+ | TA.NIntroGuess _loc ->
+ let names_ref = ref [] in
+ let s =
+ NTactics.intros_tac ~names_ref [] script#grafite_status
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
| TA.NAutoInteractive (_loc, (None,a)) ->
let trace_ref = ref [] in
let s =
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
let dbd = LibraryDb.instance () in
- let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
+ let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->