src/Pure/Thy/latex.ML
changeset 14924 2be4cbe27a27
parent 14879 8989eedf72a1
child 14973 0613f64653b7
     1.1 --- a/src/Pure/Thy/latex.ML	Sat Jun 12 22:45:35 2004 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat Jun 12 22:45:46 2004 +0200
     1.3 @@ -8,13 +8,16 @@
     1.4  
     1.5  signature LATEX =
     1.6  sig
     1.7 +  val output_known_symbols: (string -> bool) * (string -> bool) ->
     1.8 +    Symbol.symbol list -> string
     1.9    val output_symbols: Symbol.symbol list -> string
    1.10    datatype token = Basic of OuterLex.token | Markup of string | MarkupEnv of string | Verbatim
    1.11    val output_tokens: (token * string) list -> string
    1.12    val flag_markup: bool -> string
    1.13    val tex_trailer: string
    1.14    val isabelle_file: string -> string -> string
    1.15 -  val old_symbol_source: string -> Symbol.symbol list -> string
    1.16 +  val symbol_source: (string -> bool) * (string -> bool) ->
    1.17 +    string -> Symbol.symbol list -> string
    1.18    val theory_entry: string -> string
    1.19    val modes: string list
    1.20  end;
    1.21 @@ -64,16 +67,19 @@
    1.22    "~" => "{\\isachartilde}" |
    1.23    c => if Symbol.is_digit c then enclose "{\\isadigit{" "}}" c else c;
    1.24  
    1.25 -fun output_sym sym =
    1.26 +val output_chrs = translate_string output_chr;
    1.27 +
    1.28 +fun output_known_sym (known_sym, known_ctrl) sym =
    1.29    (case Symbol.decode sym of
    1.30      Symbol.Char s => output_chr s
    1.31 -  | Symbol.Sym s => enclose "{\\isasym" "}" s
    1.32 -  | Symbol.Ctrl s => enclose "\\isactrl" " " s
    1.33 +  | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
    1.34 +  | Symbol.Ctrl s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
    1.35    | Symbol.Raw s => s);
    1.36  
    1.37  in
    1.38  
    1.39 -val output_symbols = implode o map output_sym;
    1.40 +val output_known_symbols = implode oo (map o output_known_sym);
    1.41 +val output_symbols = output_known_symbols (K true, K true);
    1.42  val output_syms = output_symbols o Symbol.explode;
    1.43  
    1.44  end;
    1.45 @@ -130,8 +136,9 @@
    1.46    \\\def\\isabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    1.47    "\\end{isabellebody}%\n" ^ tex_trailer;
    1.48  
    1.49 -fun old_symbol_source name syms =
    1.50 -  isabelle_file name ("\\isamarkupheader{" ^ output_syms name ^ "}%\n" ^ output_symbols syms);
    1.51 +fun symbol_source known name syms = isabelle_file name
    1.52 +  ("\\isamarkupheader{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
    1.53 +    output_known_symbols known syms);
    1.54  
    1.55  fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
    1.56