# HG changeset patch
# User wenzelm
# Date 1199631469 -3600
# Node ID 8943e72bf92ac8720c6b17dc00d063e2131ddf1a
# Parent  af0c90f54ebe10d392c6f8e8252625d23d0f7e9b
removed obsolete prompt and channel markups;

diff -r af0c90f54ebe -r 8943e72bf92a src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jan 05 23:05:29 2008 +0100
+++ b/src/Pure/General/markup.ML	Sun Jan 06 15:57:49 2008 +0100
@@ -56,17 +56,10 @@
   val whitespaceN: string val whitespace: T
   val junkN: string val junk: T
   val commandspanN: string val commandspan: string -> T
-  val promptN: string val prompt: T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
   val hiliteN: string val hilite: T
-  val writelnN: string val writeln: T
-  val priorityN: string val priority: T
-  val tracingN: string val tracing: T
-  val warningN: string val warning: T
-  val errorN: string val error: T
-  val debugN: string val debug: T
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -177,23 +170,12 @@
 
 (* toplevel *)
 
-val (promptN, prompt) = markup_elem "prompt";
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
 val (sendbackN, sendback) = markup_elem "sendback";
 val (hiliteN, hilite) = markup_elem "hilite";
 
 
-(* channels *)
-
-val (writelnN, writeln) = markup_elem "writeln";
-val (priorityN, priority) = markup_elem "priority";
-val (tracingN, tracing) = markup_elem "tracing";
-val (warningN, warning) = markup_elem "warning";
-val (errorN, error) = markup_elem "error";
-val (debugN, debug) = markup_elem "debug";
-
-
 (* print mode operations *)
 
 fun default_output (_: T) = ("", "");