--- a/src/Pure/General/output.ML Tue Mar 14 22:06:31 2006 +0100
+++ b/src/Pure/General/output.ML Tue Mar 14 22:06:33 2006 +0100
@@ -42,6 +42,8 @@
val has_mode: string -> bool
val output_width: string -> string * real
val output: string -> string
+ val keyword_width: bool -> string -> string * real
+ val keyword: bool -> string -> string
val indent: string * int -> string
val raw: string -> string
exception TOPLEVEL_ERROR
@@ -53,7 +55,8 @@
val debug: string -> unit
val error_msg: string -> unit
val add_mode: string ->
- (string -> string * real) * (string * int -> string) * (string -> string) -> unit
+ (string -> string * real) * (bool -> string -> string * real) *
+ (string * int -> string) * (string -> string) -> unit
val accumulated_time: unit -> unit
end;
@@ -67,7 +70,8 @@
fun has_mode s = s mem_string ! print_mode;
type mode_fns =
- {output_width: string -> string * real,
+ {output: string -> string * real,
+ keyword: bool -> string -> string * real,
indent: string * int -> string,
raw: string -> string};
@@ -83,8 +87,10 @@
(case lookup_mode "" of SOME p => p
| NONE => raise MISSING_DEFAULT_OUTPUT)); (*sys_error would require output again!*)
-fun output_width x = #output_width (get_mode ()) x;
+fun output_width x = #output (get_mode ()) x;
val output = #1 o output_width;
+fun keyword_width b x = #keyword (get_mode ()) b x;
+val keyword = #1 oo keyword_width;
fun indent x = #indent (get_mode ()) x;
fun raw x = #raw (get_mode ()) x;
@@ -162,10 +168,11 @@
(* add_mode *)
-fun add_mode name (f, g, h) =
+fun add_mode name (output, keyword, indent, raw) =
(if is_none (lookup_mode name) then ()
else warning ("Redeclaration of symbol print mode: " ^ quote name);
- modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
+ change modes (Symtab.update (name,
+ {output = output, keyword = keyword, indent = indent, raw = raw})));