# HG changeset patch
# User wenzelm
# Date 1142370393 -3600
# Node ID cae36e16f3c071aec3a09d8916f228b0c4168f96
# Parent  61e775c03ed8d9804bbf3f0a43e1d393b676d4d3
Output.add_mode: keyword component;

diff -r 61e775c03ed8 -r cae36e16f3c0 src/Pure/General/output.ML
--- 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})));
 
 
 
diff -r 61e775c03ed8 -r cae36e16f3c0 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Mar 14 22:06:31 2006 +0100
+++ b/src/Pure/General/symbol.ML	Tue Mar 14 22:06:33 2006 +0100
@@ -54,6 +54,7 @@
   val bump_string: string -> string
   val length: symbol list -> int
   val default_output: string -> string * real
+  val default_keyword: bool -> string -> string * real
   val default_indent: string * int -> string
   val default_raw: string -> string
   val xsymbolsN: string
@@ -480,10 +481,11 @@
 (* default *)
 
 fun default_output s = (s, real (size s));
+fun default_keyword (_: bool) = default_output;
 fun default_indent (_: string, k) = spaces k;
 fun default_raw (s: string) = s;
 
-val _ = Output.add_mode "" (default_output, default_indent, default_raw);
+val _ = Output.add_mode "" (default_output, default_keyword, default_indent, default_raw);
 
 
 (* xsymbols *)
diff -r 61e775c03ed8 -r cae36e16f3c0 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Mar 14 22:06:31 2006 +0100
+++ b/src/Pure/Thy/html.ML	Tue Mar 14 22:06:33 2006 +0100
@@ -236,9 +236,6 @@
 end;
 
 
-val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.encode_raw);
-
-
 (* token translations *)
 
 fun style s =
@@ -265,9 +262,10 @@
 (* atoms *)
 
 val plain = output;
-fun name s = "<span class=\"name\">" ^ output s ^ "</span>";
-fun keyword s = "<span class=\"keyword\">" ^ output s ^ "</span>";
-fun file_name s = "<span class=\"filename\">" ^ output s ^ "</span>";
+val name = enclose "<span class=\"name\">" "</span>" o output;
+val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
+val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
+val file_name = enclose "<span class=\"filename\">" "</span>" o output;
 val file_path = file_name o Url.pack;
 
 
@@ -440,4 +438,9 @@
 fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
 
 
+(* mode output *)
+
+val _ = Output.add_mode htmlN
+  (output_width, K keyword_width, Symbol.default_indent, Symbol.encode_raw);
+
 end;
diff -r 61e775c03ed8 -r cae36e16f3c0 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:31 2006 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:33 2006 +0100
@@ -160,10 +160,12 @@
   let val syms = Symbol.explode str
   in (output_symbols syms, real (Symbol.length syms)) end;
 
+fun latex_keyword cmd =
+  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
+
 fun latex_indent "" = ""
   | latex_indent s = enclose "\\isaindent{" "}" s;
 
-val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw);
-
+val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
 
 end;
diff -r 61e775c03ed8 -r cae36e16f3c0 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Mar 14 22:06:31 2006 +0100
+++ b/src/Pure/proof_general.ML	Tue Mar 14 22:06:33 2006 +0100
@@ -95,11 +95,11 @@
 
 fun setup_xsymbols_output () =
   Output.add_mode xsymbolsN
-    (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
+    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
 
 fun setup_pgml_output () =
   Output.add_mode pgmlN
-    (pgml_output, Symbol.default_indent, Symbol.encode_raw);
+    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
 
 end;