moved test_markup here;
authorwenzelm
Thu Apr 03 21:23:41 2008 +0200 (2008-04-03)
changeset 265499838e45c6e6c
parent 26548 41bbcaf3e481
child 26550 a8740ad422d2
moved test_markup here;
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 03 21:23:39 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Apr 03 21:23:41 2008 +0200
     1.3 @@ -3,11 +3,12 @@
     1.4      Author:     David Aspinall and Markus Wenzel
     1.5  
     1.6  Isabelle/Isar configuration for Emacs Proof General.
     1.7 -See http://proofgeneral.inf.ed.ac.uk
     1.8 +See also http://proofgeneral.inf.ed.ac.uk
     1.9  *)
    1.10  
    1.11  signature PROOF_GENERAL =
    1.12  sig
    1.13 +  val test_markupN: string
    1.14    val init: bool -> unit
    1.15    val init_outer_syntax: unit -> unit
    1.16    val sendback: string -> Pretty.T list -> unit
    1.17 @@ -22,6 +23,9 @@
    1.18  val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
    1.19  val pgasciiN = "PGASCII";                  (*plain 7-bit ASCII communication*)
    1.20  val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    1.21 +val test_markupN = "test_markup";          (*XML markup for everything*)
    1.22 +
    1.23 +val _ = Markup.add_mode test_markupN XML.output_markup;
    1.24  
    1.25  fun special oct =
    1.26    if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
    1.27 @@ -107,7 +111,7 @@
    1.28        else if name = Markup.hiliteN then (special "327", special "330")
    1.29        else ("", "");
    1.30      val (bg2, en2) =
    1.31 -      if print_mode_active IsabelleProcess.test_markupN
    1.32 +      if print_mode_active test_markupN
    1.33        then XML.output_markup (name, props)
    1.34        else ("", "");
    1.35    in (bg1 ^ bg2, en2 ^ en1) end;