use ThySyn.add_syntax;
authorwenzelm
Wed Aug 06 11:57:52 1997 +0200 (1997-08-06)
changeset 362285898be702b2
parent 3621 d3e248853428
child 3623 e843c1d6f9e1
use ThySyn.add_syntax;
src/HOL/thy_syntax.ML
src/HOLCF/ax_ops/thy_syntax.ML
src/HOLCF/domain/interface.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  (*the kind of distinctiveness axioms depends on number of constructors*)
     1.5  val dtK = 7;  (* FIXME rename?, move? *)
     1.6  
     1.7 -structure ThySynData: THY_SYN_DATA =
     1.8 -struct
     1.9 +
    1.10 +local
    1.11  
    1.12  open ThyParse;
    1.13  
    1.14 @@ -259,13 +259,12 @@
    1.15  
    1.16  
    1.17  
    1.18 -
    1.19 -
    1.20 -(** sections **)
    1.21 +(** augment thy syntax **)
    1.22  
    1.23 -val user_keywords = ["intrs", "monos", "con_defs", "congs", "simpset", "|"];
    1.24 +in
    1.25  
    1.26 -val user_sections =
    1.27 +val _ = ThySyn.add_syntax
    1.28 + ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
    1.29   [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
    1.30    ("inductive", inductive_decl ""),
    1.31    ("coinductive", inductive_decl "Co"),
    1.32 @@ -273,10 +272,4 @@
    1.33    ("primrec", primrec_decl),
    1.34    ("recdef", rec_decl)];
    1.35  
    1.36 -
    1.37  end;
    1.38 -
    1.39 -
    1.40 -structure ThySyn = ThySynFun(ThySynData);
    1.41 -set_parser ThySyn.parse;
    1.42 -
     2.1 --- a/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
     2.2 +++ b/src/HOLCF/ax_ops/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
     2.3 @@ -5,26 +5,6 @@
     2.4  Additional thy file sections for HOLCF: axioms, ops.
     2.5  *)
     2.6  
     2.7 -(* use "holcflogics.ML"; 
     2.8 -   use "thy_axioms.ML";
     2.9 -   use "thy_ops.ML";      should already have been done in ROOT.ML *)
    2.10 -
    2.11 -structure ThySynData : THY_SYN_DATA =
    2.12 -struct
    2.13 -
    2.14 -open HOLCFlogic;
    2.15 -
    2.16 -val user_keywords = (*####*)filter_out (fn s => s mem (ThyAxioms.axioms_keywords@
    2.17 -                    ThyOps.ops_keywords)) (*####*)ThySynData.user_keywords @ 
    2.18 -                    ThyAxioms.axioms_keywords @ 
    2.19 -                    ThyOps.ops_keywords;
    2.20 -
    2.21 -val user_sections = (*####*)filter_out (fn (s,_) => s mem (map fst (
    2.22 -                    ThyAxioms.axioms_sections@ ThyOps.ops_sections))) (*####*)
    2.23 -                      ThySynData.user_sections @
    2.24 -                    ThyAxioms.axioms_sections @
    2.25 -                    ThyOps.ops_sections;
    2.26 -end;
    2.27 -
    2.28 -structure ThySyn = ThySynFun(ThySynData);
    2.29 -set_parser ThySyn.parse;
    2.30 +ThySyn.add_syntax
    2.31 + (ThyAxioms.axioms_keywords @ ThyOps.ops_keywords)
    2.32 + (ThyAxioms.axioms_sections @ ThyOps.ops_sections);
     3.1 --- a/src/HOLCF/domain/interface.ML	Wed Aug 06 11:57:20 1997 +0200
     3.2 +++ b/src/HOLCF/domain/interface.ML	Wed Aug 06 11:57:52 1997 +0200
     3.3 @@ -6,11 +6,6 @@
     3.4  parser for domain section
     3.5  *)
     3.6  
     3.7 -
     3.8 -structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *)
     3.9 -
    3.10 -struct
    3.11 -
    3.12  local 
    3.13    open ThyParse;
    3.14    open Domain_Library;
    3.15 @@ -157,14 +152,9 @@
    3.16    val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
    3.17  		    (enum1 "," (name'   --$$ "by" -- !!
    3.18  			       (enum1 "|" name'))) >> mk_gen_by;
    3.19 -end; (* local *)
    3.20  
    3.21 -val user_keywords = "lazy"::"by"::"finite"::
    3.22 -		(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**)
    3.23 -		    ThySynData.user_keywords;
    3.24 -val user_sections = ("domain", domain_decl)::("generated", gen_by_decl)::
    3.25 -		(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**)
    3.26 -		    ThySynData.user_sections;
    3.27 -end; (* struct *)
    3.28 +  val _ = ThySyn.add_syntax
    3.29 +    ["lazy", "by", "finite"]
    3.30 +    [("domain", domain_decl), ("generated", gen_by_decl)]
    3.31  
    3.32 -structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *)
    3.33 +end; (* local *)
     4.1 --- a/src/ZF/thy_syntax.ML	Wed Aug 06 11:57:20 1997 +0200
     4.2 +++ b/src/ZF/thy_syntax.ML	Wed Aug 06 11:57:52 1997 +0200
     4.3 @@ -3,11 +3,11 @@
     4.4      Author:     Lawrence C Paulson
     4.5      Copyright   1994  University of Cambridge
     4.6  
     4.7 -Additional theory file sections for ZF
     4.8 +Additional theory file sections for ZF.
     4.9  *)
    4.10  
    4.11 -structure ThySynData: THY_SYN_DATA =
    4.12 -struct
    4.13 +
    4.14 +local
    4.15  
    4.16  (*Inductive definitions theory section.   co is either "" or "Co"*)
    4.17  fun inductive_decl co =
    4.18 @@ -137,18 +137,18 @@
    4.19  end;
    4.20  
    4.21  
    4.22 -(** Section specifications **)
    4.23  
    4.24 -val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
    4.25 -                     "and", "|", "<=", "domains", "intrs", "monos", 
    4.26 -                     "con_defs", "type_intrs", "type_elims"];
    4.27 +(** augment thy syntax **)
    4.28 +
    4.29 +in
    4.30  
    4.31 -val user_sections = [("inductive",  inductive_decl ""),
    4.32 -                     ("coinductive",  inductive_decl "Co"),
    4.33 -                     ("datatype",  datatype_decl ""),
    4.34 -                     ("codatatype",  datatype_decl "Co")];
    4.35 +val _ = ThySyn.add_syntax
    4.36 + ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
    4.37 +  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
    4.38 +  "type_elims"]
    4.39 + [("inductive", inductive_decl ""),
    4.40 +  ("coinductive", inductive_decl "Co"),
    4.41 +  ("datatype", datatype_decl ""),
    4.42 +  ("codatatype", datatype_decl "Co")];
    4.43 +
    4.44  end;
    4.45 -
    4.46 -
    4.47 -structure ThySyn = ThySynFun(ThySynData);
    4.48 -set_parser ThySyn.parse;