# HG changeset patch
# User wenzelm
# Date 850218635 -3600
# Node ID 1b6bc618c35600d13fb41e6bb1e86032f9747cca
# Parent  97b88cafe1e81989912edd6c63690d943de0c0e2
syntax section: added 'output' mode option;

diff -r 97b88cafe1e8 -r 1b6bc618c356 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Dec 10 12:49:02 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Dec 10 12:50:35 1996 +0100
@@ -294,19 +294,24 @@
   optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None
   -- opt_infix >> mk_type_decl;
 
-val type_decls = repeat1 (old_type_decl || type_decl) >>
-                 (mk_type_decls o flat);
+val type_decls =
+  repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
 
 
 (* consts *)
 
-val const_decls = repeat1 (names1 --$$ "::" -- !!
-                    ((string || const_type false >> quote) -- opt_mixfix)) >>
-                  (mk_big_list o map mk_triple2 o split_decls);
+val const_decls =
+  repeat1
+    (names1 --$$ "::" -- !! ((string || const_type false >> quote) -- opt_mixfix))
+  >> (mk_big_list o map mk_triple2 o split_decls);
 
-val syntax_decls =
-  optional ("(" $$-- !! (name --$$ ")")) "\"\"" -- const_decls
-    >> (fn (mode, txt) => mode ^ "\n" ^ txt);
+val opt_mode =
+  optional
+    ("(" $$-- !! (name -- optional ($$ "output" >> K "false") "true" --$$ ")"))
+    ("\"\"", "true")
+  >> mk_pair;
+
+val syntax_decls = opt_mode -- const_decls >> (fn (mode, txt) => mode ^ "\n" ^ txt);
 
 
 (* translations *)
@@ -530,8 +535,8 @@
 
 
 val pure_keywords =
- ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<",
-  "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
+ ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
+  "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
 
 val pure_sections =
  [section "oracle" "|> set_oracle" (name >> strip_quotes),