diff -r 41bbcaf3e481 -r 9838e45c6e6c src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 03 21:23:39 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Apr 03 21:23:41 2008 +0200 @@ -3,11 +3,12 @@ Author: David Aspinall and Markus Wenzel Isabelle/Isar configuration for Emacs Proof General. -See http://proofgeneral.inf.ed.ac.uk +See also http://proofgeneral.inf.ed.ac.uk *) signature PROOF_GENERAL = sig + val test_markupN: string val init: bool -> unit val init_outer_syntax: unit -> unit val sendback: string -> Pretty.T list -> unit @@ -22,6 +23,9 @@ val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*) val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*) val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) +val test_markupN = "test_markup"; (*XML markup for everything*) + +val _ = Markup.add_mode test_markupN XML.output_markup; fun special oct = if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167) @@ -107,7 +111,7 @@ else if name = Markup.hiliteN then (special "327", special "330") else ("", ""); val (bg2, en2) = - if print_mode_active IsabelleProcess.test_markupN + if print_mode_active test_markupN then XML.output_markup (name, props) else ("", ""); in (bg1 ^ bg2, en2 ^ en1) end;