mixfix: added syntax for Infirl/rName;
authorwenzelm
Mon Nov 18 17:31:14 1996 +0100 (1996-11-18)
changeset 2203c2dbdc2ef781
parent 2202 cc15a7bfbe12
child 2204 64cb98f841e4
mixfix: added syntax for Infirl/rName;
syntax section: added option printer table name;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Nov 18 17:30:44 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 18 17:31:14 1996 +0100
     1.3 @@ -209,14 +209,14 @@
     1.4  
     1.5  (* mixfix annotations *)
     1.6  
     1.7 -val infxl = "infixl" $$-- !! nat >> cat "Infixl";
     1.8 -val infxr = "infixr" $$-- !! nat >> cat "Infixr";
     1.9 +val infxl =
    1.10 +  "infixl" $$-- !! (nat >> cat "Infixl" || string -- nat >> (cat "InfixlName" o mk_pair));
    1.11 +val infxr =
    1.12 +  "infixr" $$-- !! (nat >> cat "Infixr" || string -- nat >> (cat "InfixrName" o mk_pair));
    1.13  
    1.14  val binder = "binder" $$--
    1.15 -  !! (string -- ( ("[" $$-- nat --$$ "]") -- nat
    1.16 -                || nat >> (fn n => (n,n))
    1.17 -     )          )
    1.18 -  >> (cat "Binder" o mk_triple2);
    1.19 +  !! (string -- (("[" $$-- nat --$$ "]") -- nat || nat >> (fn n => (n, n))))
    1.20 +    >> (cat "Binder" o mk_triple2);
    1.21  
    1.22  val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
    1.23  
    1.24 @@ -304,6 +304,10 @@
    1.25                      ((string || const_type false >> quote) -- opt_mixfix)) >>
    1.26                    (mk_big_list o map mk_triple2 o split_decls);
    1.27  
    1.28 +val syntax_decls =
    1.29 +  optional ("(" $$-- !! (name --$$ ")")) "\"\"" -- const_decls
    1.30 +    >> (fn (mode, txt) => mode ^ "\n" ^ txt);
    1.31 +
    1.32  
    1.33  (* translations *)
    1.34  
    1.35 @@ -316,8 +320,8 @@
    1.36    $$ "==" >> K "Syntax.<-> ";
    1.37  
    1.38  val trans_line =
    1.39 -    trans_pat -- !! (trans_arrow -- trans_pat) >>
    1.40 -        (fn (left, (arr, right)) => arr ^ "(" ^ left ^ ",\t" ^ right ^ ")");
    1.41 +  trans_pat -- !! (trans_arrow -- trans_pat)
    1.42 +    >> (fn (left, (arr, right)) => arr ^ mk_pair (left, right));
    1.43  
    1.44  val trans_decls = repeat1 trans_line >> mk_big_list;
    1.45  
    1.46 @@ -529,7 +533,7 @@
    1.47    section "types" "" type_decls,
    1.48    section "arities" "|> add_arities" arity_decls,
    1.49    section "consts" "|> add_consts" const_decls,
    1.50 -  section "syntax" "|> add_syntax" const_decls,
    1.51 +  section "syntax" "|> add_modesyntax" syntax_decls,
    1.52    section "translations" "|> add_trrules" trans_decls,
    1.53    section "MLtrans" "|> add_trfuns" mltrans,
    1.54    section "MLtext" "" verbatim,