# HG changeset patch
# User wenzelm
# Date 1116782778 -7200
# Node ID b645ff0c697c95d9c56331b723aeeebc4c8d864b
# Parent  13f230daa195c4aac2e5fca4ec1c09ef632b6c9e
tuned;

diff -r 13f230daa195 -r b645ff0c697c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun May 22 19:26:17 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun May 22 19:26:18 2005 +0200
@@ -5,12 +5,7 @@
 Isar/Pure outer syntax.
 *)
 
-signature ISAR_SYN =
-sig
-  val keywords: string list
-  val parsers: OuterSyntax.parser list
-  val hidden_commands: string list
-end;
+signature ISAR_SYN = sig end;
 
 structure IsarSyn: ISAR_SYN =
 struct
@@ -647,7 +642,7 @@
   P.term >> FindTheorems.Pattern;
 
 val find_theoremsP =
-  OuterSyntax.improper_command "thms_containing"  (* FIXME rename to "find_theorems" *)
+  OuterSyntax.improper_command "thms_containing"
     "print theorems meeting specified criteria" K.diag
     (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
@@ -787,7 +782,7 @@
 (*keep keywords consistent with the parsers, including those in
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
-val keywords =
+val _ = OuterSyntax.add_keywords
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
   "binder", "concl", "defines", "files", "fixes", "imports", "in", "includes",
@@ -796,7 +791,7 @@
   "\\<leftharpoondown>", "\\<rightharpoonup>",
   "\\<rightleftharpoons>", "\\<subseteq>"];
 
-val parsers = [
+val _ = OuterSyntax.add_parsers [
   (*theory structure*)
   theoryP, end_excursionP, contextP,
   (*markup commands*)
@@ -832,14 +827,10 @@
   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 = [
+val _ = IsarOutput.add_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"];
+  "typed_print_translation", "print_ast_translation",
+  "token_translation"];
 
 end;
-
-OuterSyntax.add_keywords IsarSyn.keywords;
-OuterSyntax.add_parsers IsarSyn.parsers;
-IsarOutput.add_hidden_commands IsarSyn.hidden_commands;