Output.add_mode: keyword component;
authorwenzelm
Tue Mar 14 22:06:33 2006 +0100 (2006-03-14)
changeset 19265cae36e16f3c0
parent 19264 61e775c03ed8
child 19266 2e8ad3f2cd66
Output.add_mode: keyword component;
src/Pure/General/output.ML
src/Pure/General/symbol.ML
src/Pure/Thy/html.ML
src/Pure/Thy/latex.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/General/output.ML	Tue Mar 14 22:06:31 2006 +0100
     1.2 +++ b/src/Pure/General/output.ML	Tue Mar 14 22:06:33 2006 +0100
     1.3 @@ -42,6 +42,8 @@
     1.4    val has_mode: string -> bool
     1.5    val output_width: string -> string * real
     1.6    val output: string -> string
     1.7 +  val keyword_width: bool -> string -> string * real
     1.8 +  val keyword: bool -> string -> string
     1.9    val indent: string * int -> string
    1.10    val raw: string -> string
    1.11    exception TOPLEVEL_ERROR
    1.12 @@ -53,7 +55,8 @@
    1.13    val debug: string -> unit
    1.14    val error_msg: string -> unit
    1.15    val add_mode: string ->
    1.16 -    (string -> string * real) * (string * int -> string) * (string -> string) -> unit
    1.17 +    (string -> string * real) * (bool -> string -> string * real) *
    1.18 +    (string * int -> string) * (string -> string) -> unit
    1.19    val accumulated_time: unit -> unit
    1.20  end;
    1.21  
    1.22 @@ -67,7 +70,8 @@
    1.23  fun has_mode s = s mem_string ! print_mode;
    1.24  
    1.25  type mode_fns =
    1.26 - {output_width: string -> string * real,
    1.27 + {output: string -> string * real,
    1.28 +  keyword: bool -> string -> string * real,
    1.29    indent: string * int -> string,
    1.30    raw: string -> string};
    1.31  
    1.32 @@ -83,8 +87,10 @@
    1.33        (case lookup_mode "" of SOME p => p
    1.34        | NONE => raise MISSING_DEFAULT_OUTPUT));  (*sys_error would require output again!*)
    1.35  
    1.36 -fun output_width x = #output_width (get_mode ()) x;
    1.37 +fun output_width x = #output (get_mode ()) x;
    1.38  val output = #1 o output_width;
    1.39 +fun keyword_width b x = #keyword (get_mode ()) b x;
    1.40 +val keyword = #1 oo keyword_width;
    1.41  fun indent x = #indent (get_mode ()) x;
    1.42  fun raw x = #raw (get_mode ()) x;
    1.43  
    1.44 @@ -162,10 +168,11 @@
    1.45  
    1.46  (* add_mode *)
    1.47  
    1.48 -fun add_mode name (f, g, h) =
    1.49 +fun add_mode name (output, keyword, indent, raw) =
    1.50   (if is_none (lookup_mode name) then ()
    1.51    else warning ("Redeclaration of symbol print mode: " ^ quote name);
    1.52 -  modes := Symtab.update (name, {output_width = f, indent = g, raw = h}) (! modes));
    1.53 +  change modes (Symtab.update (name,
    1.54 +    {output = output, keyword = keyword, indent = indent, raw = raw})));
    1.55  
    1.56  
    1.57  
     2.1 --- a/src/Pure/General/symbol.ML	Tue Mar 14 22:06:31 2006 +0100
     2.2 +++ b/src/Pure/General/symbol.ML	Tue Mar 14 22:06:33 2006 +0100
     2.3 @@ -54,6 +54,7 @@
     2.4    val bump_string: string -> string
     2.5    val length: symbol list -> int
     2.6    val default_output: string -> string * real
     2.7 +  val default_keyword: bool -> string -> string * real
     2.8    val default_indent: string * int -> string
     2.9    val default_raw: string -> string
    2.10    val xsymbolsN: string
    2.11 @@ -480,10 +481,11 @@
    2.12  (* default *)
    2.13  
    2.14  fun default_output s = (s, real (size s));
    2.15 +fun default_keyword (_: bool) = default_output;
    2.16  fun default_indent (_: string, k) = spaces k;
    2.17  fun default_raw (s: string) = s;
    2.18  
    2.19 -val _ = Output.add_mode "" (default_output, default_indent, default_raw);
    2.20 +val _ = Output.add_mode "" (default_output, default_keyword, default_indent, default_raw);
    2.21  
    2.22  
    2.23  (* xsymbols *)
     3.1 --- a/src/Pure/Thy/html.ML	Tue Mar 14 22:06:31 2006 +0100
     3.2 +++ b/src/Pure/Thy/html.ML	Tue Mar 14 22:06:33 2006 +0100
     3.3 @@ -236,9 +236,6 @@
     3.4  end;
     3.5  
     3.6  
     3.7 -val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.encode_raw);
     3.8 -
     3.9 -
    3.10  (* token translations *)
    3.11  
    3.12  fun style s =
    3.13 @@ -265,9 +262,10 @@
    3.14  (* atoms *)
    3.15  
    3.16  val plain = output;
    3.17 -fun name s = "<span class=\"name\">" ^ output s ^ "</span>";
    3.18 -fun keyword s = "<span class=\"keyword\">" ^ output s ^ "</span>";
    3.19 -fun file_name s = "<span class=\"filename\">" ^ output s ^ "</span>";
    3.20 +val name = enclose "<span class=\"name\">" "</span>" o output;
    3.21 +val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
    3.22 +val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
    3.23 +val file_name = enclose "<span class=\"filename\">" "</span>" o output;
    3.24  val file_path = file_name o Url.pack;
    3.25  
    3.26  
    3.27 @@ -440,4 +438,9 @@
    3.28  fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
    3.29  
    3.30  
    3.31 +(* mode output *)
    3.32 +
    3.33 +val _ = Output.add_mode htmlN
    3.34 +  (output_width, K keyword_width, Symbol.default_indent, Symbol.encode_raw);
    3.35 +
    3.36  end;
     4.1 --- a/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:31 2006 +0100
     4.2 +++ b/src/Pure/Thy/latex.ML	Tue Mar 14 22:06:33 2006 +0100
     4.3 @@ -160,10 +160,12 @@
     4.4    let val syms = Symbol.explode str
     4.5    in (output_symbols syms, real (Symbol.length syms)) end;
     4.6  
     4.7 +fun latex_keyword cmd =
     4.8 +  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
     4.9 +
    4.10  fun latex_indent "" = ""
    4.11    | latex_indent s = enclose "\\isaindent{" "}" s;
    4.12  
    4.13 -val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw);
    4.14 -
    4.15 +val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
    4.16  
    4.17  end;
     5.1 --- a/src/Pure/proof_general.ML	Tue Mar 14 22:06:31 2006 +0100
     5.2 +++ b/src/Pure/proof_general.ML	Tue Mar 14 22:06:33 2006 +0100
     5.3 @@ -95,11 +95,11 @@
     5.4  
     5.5  fun setup_xsymbols_output () =
     5.6    Output.add_mode xsymbolsN
     5.7 -    (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
     5.8 +    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
     5.9  
    5.10  fun setup_pgml_output () =
    5.11    Output.add_mode pgmlN
    5.12 -    (pgml_output, Symbol.default_indent, Symbol.encode_raw);
    5.13 +    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
    5.14  
    5.15  end;
    5.16