added internal_mode;
authorwenzelm
Sat Dec 09 18:05:52 2006 +0100 (2006-12-09)
changeset 21731360fa2caaf2f
parent 21730 88d8b4052792
child 21732 4d4cde714500
added internal_mode;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Dec 09 18:05:50 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Dec 09 18:05:52 2006 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4    type mode
     1.5    val default_mode: mode
     1.6    val input_mode: mode
     1.7 +  val internal_mode: mode
     1.8    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
     1.9    val extend_const_gram: (string -> bool) ->
    1.10      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.11 @@ -187,6 +188,7 @@
    1.12  type mode = string * bool;
    1.13  val default_mode = ("", true);
    1.14  val input_mode = ("input", true);
    1.15 +val internal_mode = ("internal", true);
    1.16  
    1.17  
    1.18  (* empty_syntax *)