# HG changeset patch
# User haftmann
# Date 1390749826 -3600
# Node ID eedd549de3ef5938a916f0f24121815a1af7f6f0
# Parent  a56099a6447af7d1c651cd0899ffa0d1be05014d
more suitable names, without any notion of "activating"

diff -r a56099a6447a -r eedd549de3ef src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Jan 26 14:01:19 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sun Jan 26 16:23:46 2014 +0100
@@ -229,8 +229,8 @@
             val tyvars = intro_vars (map fst vs) reserved;
             fun requires_args classparam = case const_syntax classparam
              of NONE => NONE
-              | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
-              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
+              | SOME (_, Code_Printer.Plain_printer _) => SOME 0
+              | SOME (k, Code_Printer.Complex_printer _) => SOME k;
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
               case requires_args classparam
                of NONE => semicolon [
diff -r a56099a6447a -r eedd549de3ef src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sun Jan 26 14:01:19 2014 +0100
+++ b/src/Tools/Code/code_printer.ML	Sun Jan 26 16:23:46 2014 +0100
@@ -67,24 +67,25 @@
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
+  type raw_const_syntax
+  val plain_const_syntax: string -> raw_const_syntax
   type simple_const_syntax
+  val simple_const_syntax: simple_const_syntax -> raw_const_syntax
   type complex_const_syntax
-  type const_syntax
-  type activated_complex_const_syntax
-  datatype activated_const_syntax = Plain_const_syntax of int * string
-    | Complex_const_syntax of activated_complex_const_syntax
+  val complex_const_syntax: complex_const_syntax -> raw_const_syntax
+  val parse_const_syntax: raw_const_syntax parser
+  val requires_args: raw_const_syntax -> int
+  datatype const_printer = Plain_printer of string
+    | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
+        -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
+  type const_syntax = int * const_printer
+  val prep_const_syntax: theory -> literals
+    -> string -> raw_const_syntax -> const_syntax
   type tyco_syntax
-  val requires_args: const_syntax -> int
-  val parse_const_syntax: const_syntax parser
   val parse_tyco_syntax: tyco_syntax parser
-  val plain_const_syntax: string -> const_syntax
-  val simple_const_syntax: simple_const_syntax -> const_syntax
-  val complex_const_syntax: complex_const_syntax -> const_syntax
-  val activate_const_syntax: theory -> literals
-    -> string -> const_syntax -> activated_const_syntax
   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> (string -> activated_const_syntax option)
+    -> (string -> const_syntax option)
     -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
@@ -290,35 +291,35 @@
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
-datatype const_syntax = plain_const_syntax of string
+datatype raw_const_syntax = plain_const_syntax of string
   | complex_const_syntax of complex_const_syntax;
 
-fun requires_args (plain_const_syntax _) = 0
-  | requires_args (complex_const_syntax (k, _)) = k;
-
 fun simple_const_syntax syn =
   complex_const_syntax
     (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
 
-type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+fun requires_args (plain_const_syntax _) = 0
+  | requires_args (complex_const_syntax (k, _)) = k;
+
+datatype const_printer = Plain_printer of string
+  | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
+      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
 
-datatype activated_const_syntax = Plain_const_syntax of int * string
-  | Complex_const_syntax of activated_complex_const_syntax;
+type const_syntax = int * const_printer;
 
-fun activate_const_syntax thy literals c (plain_const_syntax s) =
-      Plain_const_syntax (Code.args_number thy c, s)
-  | activate_const_syntax thy literals c (complex_const_syntax (n, f))=
-      Complex_const_syntax (n, f literals);
+fun prep_const_syntax thy literals c (plain_const_syntax s) =
+      (Code.args_number thy c, Plain_printer s)
+  | prep_const_syntax thy literals c (complex_const_syntax (n, f))=
+      (n, Complex_printer (f literals));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     (app as ({ sym, dom, ... }, ts)) =
   case sym of
     Constant const => (case const_syntax const of
       NONE => brackify fxy (print_app_expr some_thm vars app)
-    | SOME (Plain_const_syntax (_, s)) =>
+    | SOME (_, Plain_printer s) =>
         brackify fxy (str s :: map (print_term some_thm vars BR) ts)
-    | SOME (Complex_const_syntax (k, print)) =>
+    | SOME (k, Complex_printer print) =>
         let
           fun print' fxy ts =
             print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
diff -r a56099a6447a -r eedd549de3ef src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Jan 26 14:01:19 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Jan 26 16:23:46 2014 +0100
@@ -89,11 +89,11 @@
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) sym) typargs') ts)
-          | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
+          | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR (str s) typargs') ts)
-          | SOME (Complex_const_syntax (k, print)) =>
+          | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
       in if k = l then print' fxy ts
diff -r a56099a6447a -r eedd549de3ef src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 26 14:01:19 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Jan 26 16:23:46 2014 +0100
@@ -54,11 +54,11 @@
   type identifier_data
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     -> theory -> theory
-  type const_syntax = Code_Printer.const_syntax
+  type raw_const_syntax = Code_Printer.raw_const_syntax
   type tyco_syntax = Code_Printer.tyco_syntax
-  val set_printings: (const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
+  val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     -> theory -> theory
-  val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
+  val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
   val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
   val add_class_syntax: string -> class -> string option -> theory -> theory
   val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
@@ -85,7 +85,7 @@
 type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
 
 type tyco_syntax = Code_Printer.tyco_syntax;
-type const_syntax = Code_Printer.const_syntax;
+type raw_const_syntax = Code_Printer.raw_const_syntax;
 
 
 (** checking and parsing of symbols **)
@@ -183,7 +183,7 @@
     includes: (string * Pretty.T) list,
     class_syntax: string -> string option,
     tyco_syntax: string -> Code_Printer.tyco_syntax option,
-    const_syntax: string -> Code_Printer.activated_const_syntax option }
+    const_syntax: string -> Code_Printer.const_syntax option }
   -> Code_Thingol.program
   -> serialization;
 
@@ -203,7 +203,7 @@
   description: description,
   reserved: string list,
   identifiers: identifier_data,
-  printings: (Code_Printer.activated_const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
+  printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
     (Pretty.T * string list)) Code_Symbol.data
 };
 
@@ -557,7 +557,7 @@
 fun check_const_syntax thy target c syn =
   if Code_Printer.requires_args syn > Code.args_number thy c
   then error ("Too many arguments in syntax for constant " ^ quote c)
-  else Code_Printer.activate_const_syntax thy (the_literals thy target) c syn;
+  else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
 
 fun check_tyco_syntax thy target tyco syn =
   if fst syn <> Sign.arity_number thy tyco