# HG changeset patch # User wenzelm # Date 980103245 -3600 # Node ID ea024d0254635c6e99a9bc73e2c41e54679b79ae # Parent b520e4f1313bc920cb359c66ce212e3d63b63593 added spaces; added default_indent, indent; diff -r b520e4f1313b -r ea024d025463 src/Pure/General/symbol.ML --- 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;