src/Pure/General/markup.ML
changeset 27969 46d7057b8614
parent 27894 a06f78f917e0
child 28017 4919bd124a58
     1.1 --- a/src/Pure/General/markup.ML	Sat Aug 23 23:07:36 2008 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sat Aug 23 23:07:38 2008 +0200
     1.3 @@ -82,7 +82,6 @@
     1.4    val command_spanN: string val command_span: string -> T
     1.5    val ignored_spanN: string val ignored_span: T
     1.6    val malformed_spanN: string val malformed_span: T
     1.7 -  val promptN: string val prompt: T
     1.8    val stateN: string val state: T
     1.9    val subgoalN: string val subgoal: T
    1.10    val sendbackN: string val sendback: T
    1.11 @@ -92,6 +91,19 @@
    1.12    val failedN: string val failed: T
    1.13    val finishedN: string val finished: T
    1.14    val disposedN: string val disposed: T
    1.15 +  val pidN: string
    1.16 +  val sessionN: string
    1.17 +  val classN: string
    1.18 +  val messageN: string val message: string -> T
    1.19 +  val promptN: string val prompt: T
    1.20 +  val writelnN: string
    1.21 +  val priorityN: string
    1.22 +  val tracingN: string
    1.23 +  val warningN: string
    1.24 +  val errorN: string
    1.25 +  val debugN: string
    1.26 +  val initN: string
    1.27 +  val statusN: string
    1.28    val default_output: T -> output * output
    1.29    val add_mode: string -> (T -> output * output) -> unit
    1.30    val output: T -> output * output
    1.31 @@ -156,7 +168,6 @@
    1.32  val position_properties = [lineN, columnN, offsetN] @ position_properties';
    1.33  
    1.34  val (positionN, position) = markup_elem "position";
    1.35 -
    1.36  val (locationN, location) = markup_elem "location";
    1.37  
    1.38  
    1.39 @@ -241,7 +252,6 @@
    1.40  
    1.41  (* toplevel *)
    1.42  
    1.43 -val (promptN, prompt) = markup_elem "prompt";
    1.44  val (stateN, state) = markup_elem "state";
    1.45  val (subgoalN, subgoal) = markup_elem "subgoal";
    1.46  val (sendbackN, sendback) = markup_elem "sendback";
    1.47 @@ -257,6 +267,26 @@
    1.48  val (disposedN, disposed) = markup_elem "disposed";
    1.49  
    1.50  
    1.51 +(* messages *)
    1.52 +
    1.53 +val pidN = "pid";
    1.54 +val sessionN = "session";
    1.55 +
    1.56 +val classN = "class";
    1.57 +val (messageN, message) = markup_string "message" classN;
    1.58 +
    1.59 +val (promptN, prompt) = markup_elem "prompt";
    1.60 +
    1.61 +val writelnN = "writeln";
    1.62 +val priorityN = "priority";
    1.63 +val tracingN = "tracing";
    1.64 +val warningN = "warning";
    1.65 +val errorN = "error";
    1.66 +val debugN = "debug";
    1.67 +val initN = "init";
    1.68 +val statusN = "status";
    1.69 +
    1.70 +
    1.71  (* print mode operations *)
    1.72  
    1.73  fun default_output (_: T) = ("", "");