Syntax.mode;

--- a/src/Pure/Isar/local_theory.ML	Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Sep 29 22:47:01 2006 +0200
@@ -25,8 +25,8 @@
   val naming: local_theory -> local_theory
   val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
   val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
-  val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
-  val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
+  val syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+  val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
   val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
   val consts_restricted: (string * typ -> bool) ->
     ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory

--- a/src/Pure/Isar/proof_context.ML	Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 29 22:47:01 2006 +0200
@@ -13,7 +13,7 @@
   val init: theory -> Proof.context
   val full_name: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
-  val set_syntax_mode: string * bool -> Proof.context -> Proof.context
+  val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val fact_index_of: Proof.context -> FactIndex.T
   val transfer: theory -> Proof.context -> Proof.context
@@ -137,8 +137,8 @@
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   val get_case: Proof.context -> string -> string option list -> RuleCases.T
   val expand_abbrevs: bool -> Proof.context -> Proof.context
-  val add_const_syntax: string * bool -> (string * mixfix) list -> Proof.context -> Proof.context
-  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list ->
+  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> Proof.context -> Proof.context
+  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list ->
     Proof.context -> Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b

--- a/src/Pure/Isar/specification.ML	Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Sep 29 22:47:01 2006 +0200
@@ -28,12 +28,12 @@
   val definition_i:
     ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory
-  val abbreviation: string * bool -> ((string * string option * mixfix) option * string) list ->
+  val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list ->
     local_theory -> local_theory
-  val abbreviation_i: string * bool -> ((string * typ option * mixfix) option * term) list ->
+  val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
     local_theory -> local_theory
-  val const_syntax: string * bool -> (xstring * mixfix) list -> local_theory -> local_theory
-  val const_syntax_i: string * bool -> (string * mixfix) list -> local_theory -> local_theory
+  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
+  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
 end;
 
 structure Specification: SPECIFICATION =

--- a/src/Pure/Syntax/syntax.ML	Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 29 22:47:01 2006 +0200
@@ -37,10 +37,11 @@
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val is_keyword: syntax -> string -> bool
-  val default_mode: string * bool
+  type mode
+  val default_mode: mode
   val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
   val extend_const_gram: (string -> bool) ->
-    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
+    mode -> (string * typ * mixfix) list -> syntax -> syntax
   val extend_consts: string list -> syntax -> syntax
   val extend_trfuns:
     (string * ((ast list -> ast) * stamp)) list *
@@ -54,7 +55,7 @@
     (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
   val remove_const_gram: (string -> bool) ->
-    string * bool -> (string * typ * mixfix) list -> syntax -> syntax
+    mode -> (string * typ * mixfix) list -> syntax -> syntax
   val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
   val remove_trrules: Context.generic -> (string -> bool) -> syntax ->
@@ -182,6 +183,7 @@
 
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 
+type mode = string * bool;
 val default_mode = ("", true);
 
 

--- a/src/Pure/sign.ML	Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/sign.ML	Fri Sep 29 22:47:01 2006 +0200
@@ -17,10 +17,10 @@
   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
-  val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
-  val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
-  val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
-  val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
+  val add_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
+  val add_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
+  val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
+  val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
   val add_const_constraint: xstring * string option -> theory -> theory
@@ -190,8 +190,8 @@
   val read_term: theory -> string -> term
   val read_prop: theory -> string -> term
   val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
-  val add_const_syntax: string * bool -> (string * mixfix) list -> theory -> theory
-  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list -> theory -> theory
+  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> theory -> theory
+  val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
   include SIGN_THEORY
 end
 
@@ -696,11 +696,11 @@
 
 (* modify syntax *)
 
-fun gen_syntax change_gram prep_typ prmode args thy =
+fun gen_syntax change_gram prep_typ mode args thy =
   let
     fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
       cat_error msg ("in syntax declaration " ^ quote (Syntax.const_name c mx));
-  in thy |> map_syn (change_gram (is_logtype thy) prmode (map prep args)) end;
+  in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
 
 fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
 
@@ -711,8 +711,8 @@
 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
 
-fun add_const_syntax prmode args thy =
-  thy |> add_modesyntax_i prmode (map (Consts.syntax (consts_of thy)) args);
+fun add_const_syntax mode args thy =
+  thy |> add_modesyntax_i mode (map (Consts.syntax (consts_of thy)) args);
 
 
 (* add constants *)