# HG changeset patch
# User wenzelm
# Date 1184078797 -7200
# Node ID 18d6ee42568940fafa5952c31c52a1eefd673463
# Parent  1b6a2c119151fa0dd03b97c4d9f65d55ab25af32
added print_mode setup (from pretty.ML);
removed no_state;

diff -r 1b6a2c119151 -r 18d6ee425689 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Jul 10 16:45:06 2007 +0200
+++ b/src/Pure/General/markup.ML	Tue Jul 10 16:46:37 2007 +0200
@@ -9,16 +9,16 @@
 sig
   type property = string * string
   type T = string * property list
+  val none: T
+  val properties: (string * string) list -> T -> T
   val nameN: string
   val kindN: string
-  val none: T
-  val properties: (string * string) list -> T -> T
   val lineN: string
   val fileN: string
   val positionN: string val position: T
   val indentN: string
+  val blockN: string val block: int -> T
   val widthN: string
-  val blockN: string val block: int -> T
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
   val classN: string val class: string -> T
@@ -32,8 +32,10 @@
   val commandN: string val command: string -> T
   val promptN: string val prompt: T
   val stateN: string val state: T
-  val no_stateN: string val no_state: T
   val subgoalN: string val subgoal: T
+  val default_output: T -> output * output
+  val output: T -> output * output
+  val add_mode: string -> (T -> output * output) -> unit
 end;
 
 structure Markup: MARKUP =
@@ -101,7 +103,25 @@
 
 val (promptN, prompt) = markup "prompt";
 val (stateN, state) = markup "state";
-val (no_stateN, no_state) = markup "no_state";
 val (subgoalN, subgoal) = markup "subgoal";
 
+
+(* print mode operations *)
+
+fun default_output (_: T) = ("", "");
+
+local
+  val default = {output = default_output};
+  val modes = ref (Symtab.make [("", default)]);
+in
+  fun add_mode name output =
+    change modes (Symtab.update_new (name, {output = output}));
+  fun get_mode () =
+    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
+
+fun output m =
+  if m = none then ("", "")
+  else #output (get_mode ()) m;
+
+end;