--- a/src/Pure/General/symbol.ML Sun Jan 21 19:53:29 2001 +0100
+++ b/src/Pure/General/symbol.ML Sun Jan 21 19:54:05 2001 +0100
@@ -10,6 +10,7 @@
sig
type symbol
val space: symbol
+ val spaces: int -> symbol
val sync: symbol
val is_sync: symbol -> bool
val not_sync: symbol -> bool
@@ -34,13 +35,15 @@
(symbol, (string, 'a) Source.source) Source.source
val explode: string -> symbol list
val input: string -> string
- val add_mode: string -> (string -> string * real) -> unit
+ val default_indent: string * int -> string
+ val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit
val isabelle_fontN: string
val symbolsN: string
val xsymbolsN: string
val plain_output: string -> string
val output: string -> string
val output_width: string -> string * real
+ val indent: string * int -> string
end;
structure Symbol: SYMBOL =
@@ -62,6 +65,7 @@
type symbol = string;
val space = " ";
+fun spaces k = Library.replicate_string k space;
val sync = "\\<^sync>";
val malformed = "\\<^malformed>";
val eof = "";
@@ -314,7 +318,7 @@
(** symbol output **)
-(* default_output *)
+(* default *)
fun string_size s = (s, real (size s));
@@ -322,13 +326,17 @@
if not (exists_string (equal "\\") s) then string_size s
else string_size (implode (map (fn "\\" => "\\\\" | c => c) (explode s))); (*sic!*)
+fun default_indent (_: string, k) = spaces k;
-(* isabelle_font_output *)
+
+(* isabelle_font *)
fun isabelle_font_output s =
let val cs = sym_explode s
in (implode (map char cs), real (sym_length cs)) end;
+val isabelle_font_indent = default_indent;
+
(* maintain modes *)
@@ -336,26 +344,27 @@
val symbolsN = "symbols";
val xsymbolsN = "xsymbols";
-val modes = ref (Symtab.make [(isabelle_fontN, isabelle_font_output)]);
+val modes = ref (Symtab.make [(isabelle_fontN, (isabelle_font_output, isabelle_font_indent))]);
fun lookup_mode name = Symtab.lookup (! modes, name);
-fun add_mode name f =
+fun add_mode name m =
(if is_none (lookup_mode name) then ()
else warning ("Redeclaration of symbol print mode " ^ quote name);
- modes := Symtab.update ((name, f), ! modes));
+ modes := Symtab.update ((name, m), ! modes));
+
+fun get_mode () =
+ if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent);
(* mode output *)
-fun output_width s =
- (case get_first lookup_mode (! print_mode) of
- None => default_output s
- | Some f => f s);
-
+fun output_width x = #1 (get_mode ()) x;
val output = #1 o output_width;
val plain_output = #1 o default_output;
+fun indent x = #2 (get_mode ()) x;
+
(*final declarations of this structure!*)
val length = sym_length;