# HG changeset patch
# User wenzelm
# Date 966875907 -7200
# Node ID b5e709fd1e4289e2539c295b2ee83792df07cecd
# Parent  48cefe2daf32878cc028edec18bc7db0974330d0
more \isachars;
added \isadigit;
simplified command markup;

diff -r 48cefe2daf32 -r b5e709fd1e42 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Aug 21 18:16:47 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Aug 21 18:38:27 2000 +0200
@@ -28,6 +28,8 @@
 val output_chr = fn
   " " => "\\ " |
   "\n" => "\\isanewline\n" |
+  "!" => "{\\isacharbang}" |
+  "\"" => "{\\isachardoublequote}" |
   "#" => "{\\isacharhash}" |
   "$" => "{\\isachardollar}" |
   "%" => "{\\isacharpercent}" |
@@ -36,20 +38,29 @@
   "(" => "{\\isacharparenleft}" |
   ")" => "{\\isacharparenright}" |
   "*" => "{\\isacharasterisk}" |
+  "+" => "{\\isacharplus}" |
+  "," => "{\\isacharcomma}" |
   "-" => "{\\isacharminus}" |
+  "." => "{\\isachardot}" |
+  "/" => "{\\isacharslash}" |
+  ":" => "{\\isacharcolon}" |
+  ";" => "{\\isacharsemicolon}" |
   "<" => "{\\isacharless}" |
+  "=" => "{\\isacharequal}" |
   ">" => "{\\isachargreater}" |
+  "?" => "{\\isacharquery}" |
+  "@" => "{\\isacharat}" |
   "[" => "{\\isacharbrackleft}" |
-  "\"" => "{\\isachardoublequote}" |
   "\\" => "{\\isacharbackslash}" |
   "]" => "{\\isacharbrackright}" |
   "^" => "{\\isacharcircum}" |
   "_" => "{\\isacharunderscore}" |
+  "`" => "{\\isacharbackquote}" |
   "{" => "{\\isacharbraceleft}" |
   "|" => "{\\isacharbar}" |
   "}" => "{\\isacharbraceright}" |
   "~" => "{\\isachartilde}" |
-  c => c;
+  c => if Symbol.is_digit c then enclose "\\isadigit{" "}" c else c;
 
 fun output_sym s =
   if size s = 1 then output_chr s
@@ -88,9 +99,7 @@
       let val s = T.val_of tok in
         if invisible_token tok then ""
         else if T.is_kind T.Command tok then
-          if s = "{" then "{\\isabeginblock}"
-          else if s = "}" then "{\\isaendblock}"
-          else "\\isacommand{" ^ output_syms s ^ "}"
+          "\\isacommand{" ^ output_syms s ^ "}"
         else if T.is_kind T.Keyword tok andalso Syntax.is_identifier s then
           "\\isakeyword{" ^ output_syms s ^ "}"
         else if T.is_kind T.String tok then output_syms (quote s)