src/Pure/Thy/thy_parse.ML
changeset 2360 1b6bc618c356
parent 2253 95b615550b8b
child 2385 73d1435aa729
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Dec 10 12:49:02 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Dec 10 12:50:35 1996 +0100
     1.3 @@ -294,19 +294,24 @@
     1.4    optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None
     1.5    -- opt_infix >> mk_type_decl;
     1.6  
     1.7 -val type_decls = repeat1 (old_type_decl || type_decl) >>
     1.8 -                 (mk_type_decls o flat);
     1.9 +val type_decls =
    1.10 +  repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
    1.11  
    1.12  
    1.13  (* consts *)
    1.14  
    1.15 -val const_decls = repeat1 (names1 --$$ "::" -- !!
    1.16 -                    ((string || const_type false >> quote) -- opt_mixfix)) >>
    1.17 -                  (mk_big_list o map mk_triple2 o split_decls);
    1.18 +val const_decls =
    1.19 +  repeat1
    1.20 +    (names1 --$$ "::" -- !! ((string || const_type false >> quote) -- opt_mixfix))
    1.21 +  >> (mk_big_list o map mk_triple2 o split_decls);
    1.22  
    1.23 -val syntax_decls =
    1.24 -  optional ("(" $$-- !! (name --$$ ")")) "\"\"" -- const_decls
    1.25 -    >> (fn (mode, txt) => mode ^ "\n" ^ txt);
    1.26 +val opt_mode =
    1.27 +  optional
    1.28 +    ("(" $$-- !! (name -- optional ($$ "output" >> K "false") "true" --$$ ")"))
    1.29 +    ("\"\"", "true")
    1.30 +  >> mk_pair;
    1.31 +
    1.32 +val syntax_decls = opt_mode -- const_decls >> (fn (mode, txt) => mode ^ "\n" ^ txt);
    1.33  
    1.34  
    1.35  (* translations *)
    1.36 @@ -530,8 +535,8 @@
    1.37  
    1.38  
    1.39  val pure_keywords =
    1.40 - ["end", "ML", "mixfix", "infixr", "infixl", "binder", "=", "+", ",", "<",
    1.41 -  "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.42 + ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
    1.43 +  "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>", "<="];
    1.44  
    1.45  val pure_sections =
    1.46   [section "oracle" "|> set_oracle" (name >> strip_quotes),