restored long-broken syntax sanity checks
authorhaftmann
Fri Jul 16 13:57:29 2010 +0200 (2010-07-16)
changeset 37840a3632a0b7d6c
parent 37839 b77e521e9f50
child 37841 ff1c9cb6dc5d
restored long-broken syntax sanity checks
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Fri Jul 16 13:57:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Jul 16 13:57:29 2010 +0200
     1.3 @@ -425,32 +425,32 @@
     1.4  fun read_inst thy (raw_tyco, raw_class) =
     1.5    (read_class thy raw_class, read_tyco thy raw_tyco);
     1.6  
     1.7 -fun gen_add_syntax upd del mapp check_x check_raw_syn prep_syn prep_x target raw_x some_raw_syn thy =
     1.8 +fun gen_add_syntax (mapp, upd, del) prep_x prep_syn check target raw_x some_raw_syn thy =
     1.9    let
    1.10 -    val x = prep_x thy raw_x |> tap (check_x thy);
    1.11 -    fun prep_check raw_syn = prep_syn (raw_syn |> tap (check_raw_syn thy target));
    1.12 +    val x = prep_x thy raw_x;
    1.13 +    fun make_syn raw_syn = (check thy x raw_syn: unit; prep_syn raw_syn);
    1.14    in case some_raw_syn
    1.15 -   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, prep_check raw_syn)) thy
    1.16 +   of SOME raw_syn => (map_name_syntax target o mapp) (upd (x, make_syn raw_syn)) thy
    1.17      | NONE => (map_name_syntax target o mapp) (del x) thy
    1.18    end;
    1.19  
    1.20  fun gen_add_syntax_class prep_class =
    1.21 -  gen_add_syntax Symtab.update Symtab.delete_safe (apfst o apfst) (K I) ((K o K o K) ()) I prep_class;
    1.22 +  gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class I ((K o K o K) ());
    1.23  
    1.24  fun gen_add_syntax_inst prep_inst =
    1.25 -  gen_add_syntax Symreltab.update Symreltab.delete_safe (apfst o apsnd) (K I) ((K o K o K) ()) I prep_inst;
    1.26 +  gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst I ((K o K o K) ());
    1.27  
    1.28  fun gen_add_syntax_tyco prep_tyco =
    1.29 -  gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apfst)
    1.30 +  gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco I
    1.31      (fn thy => fn tyco => fn (n, _) => if n <> Sign.arity_number thy tyco
    1.32        then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
    1.33 -      else ()) ((K o K o K) ()) I prep_tyco;
    1.34 +      else ());
    1.35  
    1.36 -fun gen_add_syntax_const prep_const check_raw_syn prep_syn =
    1.37 -  gen_add_syntax Symtab.update Symtab.delete_safe (apsnd o apsnd)
    1.38 +fun gen_add_syntax_const prep_const prep_syn check_raw_syn =
    1.39 +  gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const prep_syn
    1.40      (fn thy => fn c => fn (n, _) => if n > Code.args_number thy c
    1.41        then error ("Too many arguments in syntax for constant " ^ quote c)
    1.42 -      else ()) check_raw_syn prep_syn prep_const;
    1.43 +      else ()) check_raw_syn;
    1.44  
    1.45  fun add_reserved target =
    1.46    let
    1.47 @@ -510,8 +510,8 @@
    1.48  val add_syntax_class = gen_add_syntax_class cert_class;
    1.49  val add_syntax_inst = gen_add_syntax_inst cert_inst;
    1.50  val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
    1.51 -val add_syntax_const_simple = gen_add_syntax_const (K I) ((K o K o K) ()) Code_Printer.simple_const_syntax;
    1.52 -val add_syntax_const = gen_add_syntax_const (K I) ((K o K o K) ()) I;
    1.53 +val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
    1.54 +val add_syntax_const = gen_add_syntax_const (K I) I;
    1.55  val allow_abort = gen_allow_abort (K I);
    1.56  val add_reserved = add_reserved;
    1.57  val add_include = add_include;
    1.58 @@ -519,8 +519,8 @@
    1.59  val add_syntax_class_cmd = gen_add_syntax_class read_class;
    1.60  val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
    1.61  val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
    1.62 -val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) Code_Printer.simple_const_syntax;
    1.63 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I;
    1.64 +val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
    1.65 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
    1.66  
    1.67  val allow_abort_cmd = gen_allow_abort Code.read_const;
    1.68