src/Pure/Thy/latex.ML
changeset 9668 b5e709fd1e42
parent 9663 e4d58f1be05b
child 9707 067c25edd1bd
     1.1 --- a/src/Pure/Thy/latex.ML	Mon Aug 21 18:16:47 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Aug 21 18:38:27 2000 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4  val output_chr = fn
     1.5    " " => "\\ " |
     1.6    "\n" => "\\isanewline\n" |
     1.7 +  "!" => "{\\isacharbang}" |
     1.8 +  "\"" => "{\\isachardoublequote}" |
     1.9    "#" => "{\\isacharhash}" |
    1.10    "$" => "{\\isachardollar}" |
    1.11    "%" => "{\\isacharpercent}" |
    1.12 @@ -36,20 +38,29 @@
    1.13    "(" => "{\\isacharparenleft}" |
    1.14    ")" => "{\\isacharparenright}" |
    1.15    "*" => "{\\isacharasterisk}" |
    1.16 +  "+" => "{\\isacharplus}" |
    1.17 +  "," => "{\\isacharcomma}" |
    1.18    "-" => "{\\isacharminus}" |
    1.19 +  "." => "{\\isachardot}" |
    1.20 +  "/" => "{\\isacharslash}" |
    1.21 +  ":" => "{\\isacharcolon}" |
    1.22 +  ";" => "{\\isacharsemicolon}" |
    1.23    "<" => "{\\isacharless}" |
    1.24 +  "=" => "{\\isacharequal}" |
    1.25    ">" => "{\\isachargreater}" |
    1.26 +  "?" => "{\\isacharquery}" |
    1.27 +  "@" => "{\\isacharat}" |
    1.28    "[" => "{\\isacharbrackleft}" |
    1.29 -  "\"" => "{\\isachardoublequote}" |
    1.30    "\\" => "{\\isacharbackslash}" |
    1.31    "]" => "{\\isacharbrackright}" |
    1.32    "^" => "{\\isacharcircum}" |
    1.33    "_" => "{\\isacharunderscore}" |
    1.34 +  "`" => "{\\isacharbackquote}" |
    1.35    "{" => "{\\isacharbraceleft}" |
    1.36    "|" => "{\\isacharbar}" |
    1.37    "}" => "{\\isacharbraceright}" |
    1.38    "~" => "{\\isachartilde}" |
    1.39 -  c => c;
    1.40 +  c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c;
    1.41  
    1.42  fun output_sym s =
    1.43    if size s = 1 then output_chr s
    1.44 @@ -88,9 +99,7 @@
    1.45        let val s = T.val_of tok in
    1.46          if invisible_token tok then ""
    1.47          else if T.is_kind T.Command tok then
    1.48 -          if s = "{" then "{\\isabeginblock}"
    1.49 -          else if s = "}" then "{\\isaendblock}"
    1.50 -          else "\\isacommand{" ^ output_syms s ^ "}"
    1.51 +          "\\isacommand{" ^ output_syms s ^ "}"
    1.52          else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
    1.53            "\\isakeyword{" ^ output_syms s ^ "}"
    1.54          else if T.is_kind T.String tok then output_syms (quote s)