Symbol.encode_raw;
authorwenzelm
Sun Jun 20 09:26:48 2004 +0200 (2004-06-20)
changeset 149730613f64653b7
parent 14972 51f95648abad
child 14974 b1ecb7859c99
Symbol.encode_raw;
src/Pure/Thy/html.ML
src/Pure/Thy/latex.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/Thy/html.ML	Sun Jun 20 09:26:29 2004 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Sun Jun 20 09:26:48 2004 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.default_raw);
     1.8 +val _ = Output.add_mode htmlN (output_width, Symbol.default_indent, Symbol.encode_raw);
     1.9  
    1.10  
    1.11  (* token translations *)
     2.1 --- a/src/Pure/Thy/latex.ML	Sun Jun 20 09:26:29 2004 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Sun Jun 20 09:26:48 2004 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4  fun latex_indent "" = ""
     2.5    | latex_indent s = enclose "\\isaindent{" "}" s;
     2.6  
     2.7 -val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
     2.8 +val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.encode_raw);
     2.9  
    2.10  
    2.11  end;
     3.1 --- a/src/Pure/proof_general.ML	Sun Jun 20 09:26:29 2004 +0200
     3.2 +++ b/src/Pure/proof_general.ML	Sun Jun 20 09:26:48 2004 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4  in
     3.5  
     3.6  fun setup_xsymbols_output () = Output.add_mode proof_generalN
     3.7 -  (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.default_raw);
     3.8 +  (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
     3.9  
    3.10  end;
    3.11