# HG changeset patch
# User berghofe
# Date 1105449314 -3600
# Node ID f04179b1454beede6e6e615765dcb50351408a26
# Parent  6f4959ba7664859446e1fce4dbfb50e980f5873d
Added table of commands to be hidden in LaTeX output.

diff -r 6f4959ba7664 -r f04179b1454b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 11 14:14:39 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 11 14:15:14 2005 +0100
@@ -9,6 +9,7 @@
 sig
   val keywords: string list
   val parsers: OuterSyntax.parser list
+  val hidden_commands: string list
 end;
 
 structure IsarSyn: ISAR_SYN =
@@ -798,9 +799,17 @@
   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
+(*these commands can be hidden in LaTeX output*)
+
+val hidden_commands = [
+  "use", "ML", "ML_command", "ML_setup", "setup", "method_setup",
+  "parse_ast_translation", "parse_translation", "print_translation",
+  "typed_print_translation", "print_ast_translation", "token_translation"];
+
 end;
 
 
 (*install the Pure outer syntax*)
 OuterSyntax.add_keywords IsarSyn.keywords;
 OuterSyntax.add_parsers IsarSyn.parsers;
+IsarOutput.add_hidden_commands IsarSyn.hidden_commands;