show symbols in Isabelle/ML instead of perl;

--- a/src/Doc/Isar_Ref/Symbols.thy	Tue May 18 20:19:02 2021 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy	Tue May 18 21:09:51 2021 +0200
@@ -32,7 +32,7 @@
 
   \begin{center}
   \begin{isabellebody}
-  \input{syms}  
+  @{show_symbols}
   \end{isabellebody}
   \end{center}
 \<close>

--- a/src/Doc/Isar_Ref/document/build	Tue May 18 20:19:02 2021 +0200
+++ b/src/Doc/Isar_Ref/document/build	Tue May 18 21:09:51 2021 +0200
@@ -5,6 +5,4 @@
 FORMAT="$1"
 VARIANT="$2"
 
-./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
-

--- a/src/Doc/Isar_Ref/document/showsymbols	Tue May 18 20:19:02 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-#!/usr/bin/env perl
-
-print "\\begin{supertabular}{ll\@{\\qquad}ll}\n";
-
-$eol = "&";
-
-while (<ARGV>) {
-    if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
-        print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
-        if ("$eol" eq "&") {
-            $eol = "\\\\";
-        } else {
-            $eol = "&";
-        }
-    }
-}
-
-if ("$eol" eq "\\\\") {
-    print "$eol\n";
-}
-
-print "\\end{supertabular}\n";
-

--- a/src/Doc/ROOT	Tue May 18 20:19:02 2021 +0200
+++ b/src/Doc/ROOT	Tue May 18 21:09:51 2021 +0200
@@ -212,7 +212,6 @@
     "isar-vm.pdf"
     "isar-vm.svg"
     "root.tex"
-    "showsymbols"
     "style.sty"
 
 session JEdit (doc) in "JEdit" = HOL +

--- a/src/Doc/antiquote_setup.ML	Tue May 18 20:19:02 2021 +0200
+++ b/src/Doc/antiquote_setup.ML	Tue May 18 21:09:51 2021 +0200
@@ -207,4 +207,36 @@
 
 end;
 
+
+(* show symbols *)
+
+val _ =
+  Theory.setup (Thy_Output.antiquotation_raw \<^binding>\<open>show_symbols\<close> (Scan.succeed ())
+    (fn _ => fn _ =>
+      let
+        val symbol_name =
+          unprefix "\\newcommand{\\isasym"
+          #> raw_explode
+          #> take_prefix Symbol.is_ascii_letter
+          #> implode;
+
+        val symbols =
+          File.read \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close>
+          |> split_lines
+          |> map_filter (fn line =>
+            (case try symbol_name line of
+              NONE => NONE
+            | SOME "" => NONE
+            | SOME name => SOME ("\\verb,\\" ^ "<" ^ name ^ ">, & {\\isasym" ^ name ^ "}")));
+
+        val eol = "\\\\\n";
+        fun table (a :: b :: rest) = a ^ " & " ^ b ^ eol :: table rest
+          | table [a] = [a ^ eol]
+          | table [] = [];
+      in
+        Latex.string
+          ("\\begin{supertabular}{ll@{\\qquad}ll}\n" ^ implode (table symbols) ^
+           "\\end{supertabular}\n")
+      end))
+
 end;