# HG changeset patch
# User wenzelm
# Date 1471008325 -7200
# Node ID 88727334666e8420b3b06dd271ecade6220f7d2c
# Parent  e217525d6b649c4c405c69ba3521b1da2dee7723
more latex symbols, notably for embedded ML;

diff -r e217525d6b64 -r 88727334666e lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Aug 12 14:19:27 2016 +0200
+++ b/lib/texinputs/isabellesym.sty	Fri Aug 12 15:25:25 2016 +0200
@@ -367,3 +367,6 @@
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
+\newcommand{\isactrlundefined}{\isakeyword{undefined}\ }
+\newcommand{\isactrlfile}{\isakeyword{file}\ }
+\newcommand{\isactrldir}{\isakeyword{dir}\ }
diff -r e217525d6b64 -r 88727334666e src/Doc/Isar_Ref/document/showsymbols
--- a/src/Doc/Isar_Ref/document/showsymbols	Fri Aug 12 14:19:27 2016 +0200
+++ b/src/Doc/Isar_Ref/document/showsymbols	Fri Aug 12 15:25:25 2016 +0200
@@ -5,11 +5,13 @@
 $eol = "&";
 
 while (<ARGV>) {
-    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
-       print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
-#       print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
+    if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) {
+        if ($1 eq "isasym") {
+            print "\\verb,\\<$2>, & {\\isasym$2} $eol\n";
+        }
+        else {
+            print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n";
+        }
         if ("$eol" eq "&") {
             $eol = "\\\\";
         } else {