added print_mode setup (from pretty.ML);
authorwenzelm
Tue Jul 10 16:46:37 2007 +0200 (2007-07-10)
changeset 2370418d6ee425689
parent 23703 1b6a2c119151
child 23705 315c638d5856
added print_mode setup (from pretty.ML);
removed no_state;
src/Pure/General/markup.ML
     1.1 --- a/src/Pure/General/markup.ML	Tue Jul 10 16:45:06 2007 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Jul 10 16:46:37 2007 +0200
     1.3 @@ -9,16 +9,16 @@
     1.4  sig
     1.5    type property = string * string
     1.6    type T = string * property list
     1.7 +  val none: T
     1.8 +  val properties: (string * string) list -> T -> T
     1.9    val nameN: string
    1.10    val kindN: string
    1.11 -  val none: T
    1.12 -  val properties: (string * string) list -> T -> T
    1.13    val lineN: string
    1.14    val fileN: string
    1.15    val positionN: string val position: T
    1.16    val indentN: string
    1.17 +  val blockN: string val block: int -> T
    1.18    val widthN: string
    1.19 -  val blockN: string val block: int -> T
    1.20    val breakN: string val break: int -> T
    1.21    val fbreakN: string val fbreak: T
    1.22    val classN: string val class: string -> T
    1.23 @@ -32,8 +32,10 @@
    1.24    val commandN: string val command: string -> T
    1.25    val promptN: string val prompt: T
    1.26    val stateN: string val state: T
    1.27 -  val no_stateN: string val no_state: T
    1.28    val subgoalN: string val subgoal: T
    1.29 +  val default_output: T -> output * output
    1.30 +  val output: T -> output * output
    1.31 +  val add_mode: string -> (T -> output * output) -> unit
    1.32  end;
    1.33  
    1.34  structure Markup: MARKUP =
    1.35 @@ -101,7 +103,25 @@
    1.36  
    1.37  val (promptN, prompt) = markup "prompt";
    1.38  val (stateN, state) = markup "state";
    1.39 -val (no_stateN, no_state) = markup "no_state";
    1.40  val (subgoalN, subgoal) = markup "subgoal";
    1.41  
    1.42 +
    1.43 +(* print mode operations *)
    1.44 +
    1.45 +fun default_output (_: T) = ("", "");
    1.46 +
    1.47 +local
    1.48 +  val default = {output = default_output};
    1.49 +  val modes = ref (Symtab.make [("", default)]);
    1.50 +in
    1.51 +  fun add_mode name output =
    1.52 +    change modes (Symtab.update_new (name, {output = output}));
    1.53 +  fun get_mode () =
    1.54 +    the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    1.55  end;
    1.56 +
    1.57 +fun output m =
    1.58 +  if m = none then ("", "")
    1.59 +  else #output (get_mode ()) m;
    1.60 +
    1.61 +end;