--- a/src/Doc/antiquote_setup.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Wed Nov 05 22:39:49 2014 +0100
@@ -195,7 +195,7 @@
is_some (Keyword.command_keyword name) andalso
let
val markup =
- Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none name
+ Outer_Syntax.scan (Keyword.get_keywords ()) Position.none name
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
|> map (snd o fst);
val _ = Context_Position.reports ctxt (map (pair pos) markup);
--- a/src/HOL/Decision_Procs/MIR.thy Wed Nov 05 19:43:17 2014 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Nov 05 22:39:49 2014 +0100
@@ -5667,19 +5667,19 @@
*} "decision procedure for MIR arithmetic"
-lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
+lemma "\<forall>x::real. (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))"
by mir
-lemma "ALL (x::real). real (2::int)*x - (real (1::int)) < real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<and> real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<le> real (2::int)*x + (real (1::int))"
+lemma "\<forall>x::real. real (2::int)*x - (real (1::int)) < real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<and> real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<le> real (2::int)*x + (real (1::int))"
by mir
-lemma "ALL (x::real). 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>"
+lemma "\<forall>x::real. 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>"
by mir
-lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
+lemma "\<forall>x::real. \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)"
by mir
-lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
by mir
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 05 22:39:49 2014 +0100
@@ -535,7 +535,7 @@
fun do_method named_thms ctxt =
let
val ref_of_str =
- suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse.xthm
+ suffix ";" #> Outer_Syntax.scan (Keyword.get_keywords ()) Position.none #> Parse.xthm
#> fst
val thms = named_thms |> maps snd
val facts = named_thms |> map (ref_of_str o fst o fst)
@@ -561,7 +561,7 @@
let
val (type_encs, lam_trans) =
!meth
- |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+ |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
|> filter Token.is_proper |> tl
|> Metis_Tactic.parse_metis_options |> fst
|>> the_default [ATP_Proof_Reconstruct.partial_typesN]
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Nov 05 22:39:49 2014 +0100
@@ -221,7 +221,7 @@
val thy = Proof_Context.theory_of lthy
val dummy_thm = Thm.transfer thy Drule.dummy_thm
- val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
+ val pointer = Outer_Syntax.scan (Keyword.get_keywords ()) Position.none bundle_name
val restore_lifting_att =
([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 05 22:39:49 2014 +0100
@@ -80,7 +80,7 @@
val subgoal_count = Try.subgoal_count
fun reserved_isar_keyword_table () =
- Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
+ Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
exception TOO_MANY of unit
@@ -126,12 +126,12 @@
fun thms_of_name ctxt name =
let
- val lex = Keyword.get_lexicons
val get = maps (Proof_Context.get_fact ctxt o fst)
+ val keywords = Keyword.get_keywords ()
in
Source.of_string name
|> Symbol.source
- |> Token.source lex Position.start
+ |> Token.source keywords Position.start
|> Token.source_proper
|> Source.source Token.stopper (Parse.xthms1 >> get)
|> Source.exhaust
--- a/src/HOL/Tools/try0.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/HOL/Tools/try0.ML Wed Nov 05 22:39:49 2014 +0100
@@ -43,7 +43,7 @@
fun parse_method s =
enclose "(" ")" s
- |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+ |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
|> filter Token.is_proper
|> Scan.read Token.stopper Method.parse
|> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
--- a/src/Pure/Isar/attrib.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Nov 05 22:39:49 2014 +0100
@@ -289,9 +289,9 @@
fun read_attribs ctxt source =
let
val syms = Symbol_Pos.source_explode source;
- val lex = #1 (Keyword.get_lexicons ());
+ val keywords = Keyword.get_keywords ();
in
- (case Token.read lex Parse.attribs syms of
+ (case Token.read_no_commands keywords Parse.attribs syms of
[raw_srcs] => check_attribs ctxt raw_srcs
| _ => error ("Malformed attributes" ^ Position.here (#pos source)))
end;
--- a/src/Pure/Isar/keyword.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/keyword.ML Wed Nov 05 22:39:49 2014 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Isar/keyword.ML
Author: Makarius
-Isar command keyword classification and global keyword tables.
+Isar keyword classification.
*)
signature KEYWORD =
@@ -41,13 +41,20 @@
type spec = (string * string list) * string list
val spec: spec -> T
val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
+ type keywords
+ val minor_keywords: keywords -> Scan.lexicon
+ val major_keywords: keywords -> Scan.lexicon
+ val empty_keywords: keywords
+ val merge_keywords: keywords * keywords -> keywords
+ val no_command_keywords: keywords -> keywords
+ val add: string * T option -> keywords -> keywords
+ val define: string * T option -> unit
+ val get_keywords: unit -> keywords
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
val is_keyword: string -> bool
val command_keyword: string -> T option
val command_files: string -> Path.T -> Path.T list
val command_tags: string -> string list
- val dest: unit -> string list * string list
- val define: string * T option -> unit
val is_diag: string -> bool
val is_heading: string -> bool
val is_theory_begin: string -> bool
@@ -144,32 +151,69 @@
-(** global keyword tables **)
+(** keyword tables **)
+
+(* type keywords *)
datatype keywords = Keywords of
- {lexicons: Scan.lexicon * Scan.lexicon, (*minor, major*)
- commands: T Symtab.table}; (*command classification*)
+ {minor: Scan.lexicon,
+ major: Scan.lexicon,
+ commands: T Symtab.table};
+
+fun minor_keywords (Keywords {minor, ...}) = minor;
+fun major_keywords (Keywords {major, ...}) = major;
+fun commands (Keywords {commands, ...}) = commands;
+
+fun make_keywords (minor, major, commands) =
+ Keywords {minor = minor, major = major, commands = commands};
-fun make_keywords (lexicons, commands) =
- Keywords {lexicons = lexicons, commands = commands};
+fun map_keywords f (Keywords {minor, major, commands}) =
+ make_keywords (f (minor, major, commands));
+
+val empty_keywords =
+ make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
-local
+fun merge_keywords
+ (Keywords {minor = minor1, major = major1, commands = commands1},
+ Keywords {minor = minor2, major = major2, commands = commands2}) =
+ make_keywords
+ (Scan.merge_lexicons (minor1, minor2),
+ Scan.merge_lexicons (major1, major2),
+ Symtab.merge (K true) (commands1, commands2));
-val global_keywords =
- Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
+val no_command_keywords =
+ map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
-in
+
+(* add keywords *)
-fun get_keywords () = ! global_keywords;
+fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
+ (case opt_kind of
+ NONE =>
+ let
+ val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+ in (minor', major, commands) end
+ | SOME kind =>
+ let
+ val major' = Scan.extend_lexicon (Symbol.explode name) major;
+ val commands' = Symtab.update (name, kind) commands;
+ in (minor, major', commands') end));
-fun change_keywords f = CRITICAL (fn () =>
- Unsynchronized.change global_keywords
- (fn Keywords {lexicons, commands} => make_keywords (f (lexicons, commands))));
+
+(* global state *)
+
+local val global_keywords = Unsynchronized.ref empty_keywords in
+
+fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl));
+fun get_keywords () = ! global_keywords;
end;
-fun get_lexicons () = get_keywords () |> (fn Keywords {lexicons, ...} => lexicons);
-fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands);
+fun get_lexicons () =
+ let val keywords = get_keywords ()
+ in (minor_keywords keywords, major_keywords keywords) end;
+
+fun get_commands () = commands (get_keywords ());
(* lookup *)
@@ -192,23 +236,6 @@
val command_tags = these o Option.map tags_of o command_keyword;
-fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
-
-
-(* define *)
-
-fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
- (case opt_kind of
- NONE =>
- let
- val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
- in ((minor', major), commands) end
- | SOME kind =>
- let
- val major' = Scan.extend_lexicon (Symbol.explode name) major;
- val commands' = Symtab.update (name, kind) commands;
- in ((minor, major'), commands') end));
-
(* command categories *)
--- a/src/Pure/Isar/keyword.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Wed Nov 05 22:39:49 2014 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Isar/keyword.scala
Author: Makarius
-Isar command keyword classification and keyword tables.
+Isar keyword classification.
*/
package isabelle
@@ -9,9 +9,10 @@
object Keyword
{
+ /** keyword classification **/
+
/* kinds */
- val MINOR = "minor"
val DIAG = "diag"
val HEADING = "heading"
val THY_BEGIN = "thy_begin"
@@ -60,5 +61,74 @@
val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
val qed_global = Set(QED_GLOBAL)
+
+
+ type Spec = ((String, List[String]), List[String])
+
+
+
+ /** keyword tables **/
+
+ object Keywords
+ {
+ def empty: Keywords = new Keywords()
+ }
+
+ class Keywords private(
+ val minor: Scan.Lexicon = Scan.Lexicon.empty,
+ val major: Scan.Lexicon = Scan.Lexicon.empty,
+ commands: Map[String, (String, List[String])] = Map.empty)
+ {
+ /* content */
+
+ def is_empty: Boolean = minor.isEmpty && major.isEmpty
+
+ override def toString: String =
+ {
+ val keywords1 = minor.iterator.map(quote(_)).toList
+ val keywords2 =
+ for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
+ quote(name) + " :: " + quote(kind) +
+ (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
+ }
+ (keywords1 ::: keywords2).mkString("keywords\n ", " and\n ", "")
+ }
+
+
+ /* add keywords */
+
+ def + (name: String): Keywords = new Keywords(minor + name, major, commands)
+ def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
+ def + (name: String, kind: (String, List[String])): Keywords =
+ {
+ val major1 = major + name
+ val commands1 = commands + (name -> kind)
+ new Keywords(minor, major1, commands1)
+ }
+
+
+ /* command kind */
+
+ def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
+
+ def is_command_kind(token: Token, pred: String => Boolean): Boolean =
+ token.is_command &&
+ (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
+
+
+ /* load commands */
+
+ def load_command(name: String): Option[List[String]] =
+ commands.get(name) match {
+ case Some((THY_LOAD, exts)) => Some(exts)
+ case _ => None
+ }
+
+ private lazy val load_commands: List[(String, List[String])] =
+ (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
+
+ def load_commands_in(text: String): Boolean =
+ load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+ }
}
--- a/src/Pure/Isar/outer_syntax.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Wed Nov 05 22:39:49 2014 +0100
@@ -12,7 +12,7 @@
type syntax
val batch_mode: bool Unsynchronized.ref
val is_markup: syntax -> Thy_Output.markup -> string -> bool
- val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * syntax
+ val get_syntax: unit -> Keyword.keywords * syntax
val check_syntax: unit -> unit
type command_spec = (string * Keyword.T) * Position.T
val command: command_spec -> string ->
@@ -29,9 +29,8 @@
(local_theory -> Proof.state) parser -> unit
val help_syntax: string list -> unit
val print_syntax: unit -> unit
- val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
- val parse: (Scan.lexicon * Scan.lexicon) * syntax ->
- Position.T -> string -> Toplevel.transition list
+ val scan: Keyword.keywords -> Position.T -> string -> Token.T list
+ val parse: Keyword.keywords * syntax -> Position.T -> string -> Toplevel.transition list
val parse_spans: Token.T list -> Command_Span.span list
val side_comments: Token.T list -> Token.T list
val command_reports: syntax -> Token.T -> Position.report_text list
@@ -137,13 +136,14 @@
in
-fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_syntax));
+fun get_syntax () = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
fun check_syntax () =
let
- val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_syntax));
+ val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
+ val major = Keyword.major_keywords keywords;
in
- (case subtract (op =) (map #1 (dest_commands syntax)) major of
+ (case subtract (op =) (map #1 (dest_commands syntax)) (Scan.dest_lexicon major) of
[] => ()
| missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
end;
@@ -178,10 +178,11 @@
fun print_syntax () =
let
- val ((keywords, _), syntax) = CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
+ val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), #2 (get_syntax ())));
+ val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
val commands = dest_commands syntax;
in
- [Pretty.strs ("syntax keywords:" :: map quote keywords),
+ [Pretty.strs ("keywords:" :: map quote minor),
Pretty.big_list "commands:" (map pretty_command commands)]
|> Pretty.writeln_chunks
end;
@@ -195,7 +196,7 @@
local
fun parse_command syntax =
- Parse.position Parse.command :|-- (fn (name, pos) =>
+ Parse.position Parse.command_ :|-- (fn (name, pos) =>
let
val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
in
@@ -222,16 +223,16 @@
(* off-line scanning/parsing *)
-fun scan lexs pos =
+fun scan keywords pos =
Source.of_string #>
Symbol.source #>
- Token.source (K lexs) pos #>
+ Token.source keywords pos #>
Source.exhaust;
-fun parse (lexs, syntax) pos str =
+fun parse (keywords, syntax) pos str =
Source.of_string str
|> Symbol.source
- |> Token.source (K lexs) pos
+ |> Token.source keywords pos
|> commands_source syntax
|> Source.exhaust;
--- a/src/Pure/Isar/outer_syntax.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Wed Nov 05 22:39:49 2014 +0100
@@ -74,95 +74,58 @@
}
final class Outer_Syntax private(
- keywords: Map[String, (String, List[String])] = Map.empty,
- lexicon: Scan.Lexicon = Scan.Lexicon.empty,
+ val keywords: Keyword.Keywords = Keyword.Keywords.empty,
val completion: Completion = Completion.empty,
val language_context: Completion.Language_Context = Completion.Language_Context.outer,
val has_tokens: Boolean = true) extends Prover.Syntax
{
/** syntax content **/
- override def toString: String =
- (for ((name, (kind, files)) <- keywords) yield {
- if (kind == Keyword.MINOR) quote(name)
- else
- quote(name) + " :: " + quote(kind) +
- (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
- }).toList.sorted.mkString("keywords\n ", " and\n ", "")
+ override def toString: String = keywords.toString
- /* keyword kind */
-
- def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
- def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
+ /* add keywords */
- def is_command(name: String): Boolean =
- keyword_kind(name) match {
- case Some(kind) => kind != Keyword.MINOR
- case None => false
+ def + (name: String): Outer_Syntax = this + (name, None, None)
+ def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
+ def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
+ : Outer_Syntax =
+ {
+ val keywords1 =
+ opt_kind match {
+ case None => keywords + name
+ case Some(kind) => keywords + (name, kind)
+ }
+ val completion1 =
+ if (replace == Some("")) completion
+ else completion + (name, replace getOrElse name)
+ new Outer_Syntax(keywords1, completion1, language_context, true)
+ }
+
+ def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
+ (this /: keywords) {
+ case (syntax, (name, opt_spec, replace)) =>
+ val opt_kind = opt_spec.map(_._1)
+ syntax +
+ (Symbol.decode(name), opt_kind, replace) +
+ (Symbol.encode(name), opt_kind, replace)
}
- def command_kind(token: Token, pred: String => Boolean): Boolean =
- token.is_command && is_command(token.source) &&
- pred(keyword_kind(token.source).get)
-
/* load commands */
- def load_command(name: String): Option[List[String]] =
- keywords.get(name) match {
- case Some((Keyword.THY_LOAD, exts)) => Some(exts)
- case _ => None
- }
-
- val load_commands: List[(String, List[String])] =
- (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
-
- def load_commands_in(text: String): Boolean =
- load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
-
-
- /* add keywords */
-
- def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
- {
- val keywords1 = keywords + (name -> kind)
- val lexicon1 = lexicon + name
- val completion1 =
- if (replace == Some("")) completion
- else completion + (name, replace getOrElse name)
- new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
- }
-
- def + (name: String, kind: (String, List[String])): Outer_Syntax =
- this + (name, kind, Some(name))
- def + (name: String, kind: String): Outer_Syntax =
- this + (name, (kind, Nil), Some(name))
- def + (name: String, replace: Option[String]): Outer_Syntax =
- this + (name, (Keyword.MINOR, Nil), replace)
- def + (name: String): Outer_Syntax = this + (name, None)
-
- def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
- (this /: keywords) {
- case (syntax, (name, Some((kind, _)), replace)) =>
- syntax +
- (Symbol.decode(name), kind, replace) +
- (Symbol.encode(name), kind, replace)
- case (syntax, (name, None, replace)) =>
- syntax +
- (Symbol.decode(name), replace) +
- (Symbol.encode(name), replace)
- }
+ def load_command(name: String): Option[List[String]] = keywords.load_command(name)
+ def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
/* language context */
def set_language_context(context: Completion.Language_Context): Outer_Syntax =
- new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
+ new Outer_Syntax(keywords, completion, context, has_tokens)
def no_tokens: Outer_Syntax =
{
- require(keywords.isEmpty && lexicon.isEmpty)
+ require(keywords.is_empty)
new Outer_Syntax(
completion = completion,
language_context = language_context,
@@ -182,7 +145,7 @@
val command1 = tokens.exists(_.is_command)
val depth1 =
- if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
+ if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
else if (command1) struct.after_span_depth
else struct.span_depth
@@ -190,11 +153,16 @@
((struct.span_depth, struct.after_span_depth) /: tokens) {
case ((x, y), tok) =>
if (tok.is_command) {
- if (command_kind(tok, Keyword.theory_goal)) (2, 1)
- else if (command_kind(tok, Keyword.theory)) (1, 0)
- else if (command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) (y + 2, y + 1)
- else if (command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1)
- else if (command_kind(tok, Keyword.qed_global)) (1, 0)
+ if (keywords.is_command_kind(tok, Keyword.theory_goal))
+ (2, 1)
+ else if (keywords.is_command_kind(tok, Keyword.theory))
+ (1, 0)
+ else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
+ (y + 2, y + 1)
+ else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
+ (y + 1, y - 1)
+ else if (keywords.is_command_kind(tok, Keyword.qed_global))
+ (1, 0)
else (x, y)
}
else (x, y)
@@ -209,8 +177,7 @@
def scan(input: CharSequence): List[Token] =
{
val in: Reader[Char] = new CharSequenceReader(input)
- Token.Parsers.parseAll(
- Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), in) match {
+ Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
case Token.Parsers.Success(tokens, _) => tokens
case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
}
@@ -222,7 +189,7 @@
val toks = new mutable.ListBuffer[Token]
var ctxt = context
while (!in.atEnd) {
- Token.Parsers.parse(Token.Parsers.token_line(lexicon, is_command, ctxt), in) match {
+ Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match {
case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
case Token.Parsers.NoSuccess(_, rest) =>
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
@@ -283,7 +250,7 @@
case "subsection" => Some(2)
case "subsubsection" => Some(3)
case _ =>
- keyword_kind(command.name) match {
+ keywords.command_kind(command.name) match {
case Some(kind) if Keyword.theory(kind) => Some(4)
case _ => None
}
--- a/src/Pure/Isar/parse.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/parse.ML Wed Nov 05 22:39:49 2014 +0100
@@ -17,7 +17,7 @@
val position: 'a parser -> ('a * Position.T) parser
val source_position: 'a parser -> Symbol_Pos.source parser
val inner_syntax: 'a parser -> string parser
- val command: string parser
+ val command_: string parser
val keyword: string parser
val short_ident: string parser
val long_ident: string parser
@@ -33,7 +33,7 @@
val verbatim: string parser
val cartouche: string parser
val eof: string parser
- val command_name: string -> string parser
+ val command: string -> string parser
val keyword_with: (string -> bool) -> string parser
val keyword_markup: bool * Markup.T -> string -> string parser
val keyword_improper: string -> string parser
@@ -180,7 +180,7 @@
group (fn () => Token.str_of_kind k)
(RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
-val command = kind Token.Command;
+val command_ = kind Token.Command;
val keyword = kind Token.Keyword;
val short_ident = kind Token.Ident;
val long_ident = kind Token.LongIdent;
@@ -196,7 +196,7 @@
val cartouche = kind Token.Cartouche;
val eof = kind Token.EOF;
-fun command_name x =
+fun command x =
group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
(RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
>> Token.content_of;
--- a/src/Pure/Isar/parse.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/parse.scala Wed Nov 05 22:39:49 2014 +0100
@@ -51,7 +51,7 @@
token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
{ case (_, pos) => pos.position }
- def keyword(name: String): Parser[String] =
+ def $$$(name: String): Parser[String] =
atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
def string: Parser[String] = atom("string", _.is_string)
@@ -73,7 +73,7 @@
tok.kind == Token.Kind.IDENT ||
tok.kind == Token.Kind.STRING)
- def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
+ def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
/* wrappers */
--- a/src/Pure/Isar/token.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Nov 05 22:39:49 2014 +0100
@@ -79,16 +79,16 @@
val pretty_src: Proof.context -> src -> Pretty.T
val ident_or_symbolic: string -> bool
val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
- val source: (unit -> Scan.lexicon * Scan.lexicon) ->
+ val source: Keyword.keywords ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
- val source_strict: (unit -> Scan.lexicon * Scan.lexicon) ->
+ val source_strict: Keyword.keywords ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
type 'a parser = T list -> 'a * T list
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
- val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list -> 'a list
- val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
+ val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
+ val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
@@ -530,7 +530,7 @@
fun token_range k (pos1, (ss, pos2)) =
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
-fun scan (lex1, lex2) = !!! "bad input"
+fun scan keywords = !!! "bad input"
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
scan_verbatim >> token_range Verbatim ||
@@ -539,8 +539,8 @@
scan_space >> token Space ||
(Scan.max token_leq
(Scan.max token_leq
- (Scan.literal lex2 >> pair Command)
- (Scan.literal lex1 >> pair Keyword))
+ (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
+ (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
(Lexicon.scan_longid >> pair LongIdent ||
Lexicon.scan_id >> pair Ident ||
Lexicon.scan_var >> pair Var ||
@@ -561,14 +561,14 @@
in
-fun source' strict get_lex =
+fun source' strict keywords =
let
- val scan_strict = Scan.bulk (fn xs => scan (get_lex ()) xs);
+ val scan_strict = Scan.bulk (scan keywords);
val scan = if strict then scan_strict else Scan.recover scan_strict recover;
in Source.source Symbol_Pos.stopper scan end;
-fun source get_lex pos src = Symbol_Pos.source pos src |> source' false get_lex;
-fun source_strict get_lex pos src = Symbol_Pos.source pos src |> source' true get_lex;
+fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords;
+fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords;
end;
@@ -582,19 +582,19 @@
(* read source *)
-fun read lex scan syms =
+fun read_no_commands keywords scan syms =
Source.of_list syms
- |> source' true (K (lex, Scan.empty_lexicon))
+ |> source' true (Keyword.no_command_keywords keywords)
|> source_proper
|> Source.source stopper (Scan.error (Scan.bulk scan))
|> Source.exhaust;
-fun read_antiq lex scan (syms, pos) =
+fun read_antiq keywords scan (syms, pos) =
let
fun err msg =
cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
"@{" ^ Symbol_Pos.content syms ^ "}");
- val res = read lex scan syms handle ERROR msg => err msg;
+ val res = read_no_commands keywords scan syms handle ERROR msg => err msg;
in (case res of [x] => x | _ => err "") end;
--- a/src/Pure/Isar/token.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Isar/token.scala Wed Nov 05 22:39:49 2014 +0100
@@ -51,8 +51,7 @@
string | (alt_string | (verb | (cart | cmt)))
}
- private def other_token(lexicon: Scan.Lexicon, is_command: String => Boolean)
- : Parser[Token] =
+ private def other_token(keywords: Keyword.Keywords): Parser[Token] =
{
val letdigs1 = many1(Symbol.is_letdig)
val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
@@ -80,9 +79,9 @@
(many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
(x => Token(Token.Kind.SYM_IDENT, x))
- val command_keyword =
- literal(lexicon) ^^
- (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))
+ val keyword =
+ literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) |||
+ literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x))
val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
@@ -96,13 +95,13 @@
space | (recover_delimited |
(((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
- command_keyword) | bad))
+ keyword) | bad))
}
- def token(lexicon: Scan.Lexicon, is_command: String => Boolean): Parser[Token] =
- delimited_token | other_token(lexicon, is_command)
+ def token(keywords: Keyword.Keywords): Parser[Token] =
+ delimited_token | other_token(keywords)
- def token_line(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Line_Context)
+ def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context)
: Parser[(Token, Scan.Line_Context)] =
{
val string =
@@ -112,7 +111,7 @@
val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
- val other = other_token(lexicon, is_command) ^^ { case x => (x, Scan.Finished) }
+ val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) }
string | (alt_string | (verb | (cart | (cmt | other))))
}
--- a/src/Pure/ML/ml_context.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Nov 05 22:39:49 2014 +0100
@@ -116,14 +116,14 @@
then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
else
let
- val lex = #1 (Keyword.get_lexicons ());
+ val keywords = Keyword.get_keywords ();
fun no_decl _ = ([], []);
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
| expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
let
val (decl, ctxt') =
- apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+ apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', ctxt') end;
--- a/src/Pure/PIDE/document.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/PIDE/document.ML Wed Nov 05 22:39:49 2014 +0100
@@ -318,7 +318,7 @@
val span =
Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id)
- (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
+ (fn () => Outer_Syntax.scan (Keyword.get_keywords ()) (Position.id id) text) ());
val _ =
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
--- a/src/Pure/PIDE/resources.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/PIDE/resources.ML Wed Nov 05 22:39:49 2014 +0100
@@ -147,9 +147,9 @@
let
val {name = (name, _), ...} = header;
val _ = Thy_Header.define_keywords header;
+ val keywords = Keyword.get_keywords ();
- val lexs = Keyword.get_lexicons ();
- val toks = Outer_Syntax.scan lexs text_pos text;
+ val toks = Outer_Syntax.scan keywords text_pos text;
val spans = Outer_Syntax.parse_spans toks;
val elements = Thy_Syntax.parse_elements spans;
@@ -165,13 +165,13 @@
fun present () =
let
val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
- val ((minor, _), syntax) = Outer_Syntax.get_syntax ();
+ val (keywords, syntax) = Outer_Syntax.get_syntax ();
in
if exists (Toplevel.is_skipped_proof o #2) res then
warning ("Cannot present theory with skipped proofs: " ^ quote name)
else
let val tex_source =
- Thy_Output.present_thy minor Keyword.command_tags
+ Thy_Output.present_thy keywords Keyword.command_tags
(Outer_Syntax.is_markup syntax) res toks
|> Buffer.content;
in if document then Present.theory_output name tex_source else () end
--- a/src/Pure/ROOT.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/ROOT.ML Wed Nov 05 22:39:49 2014 +0100
@@ -230,8 +230,8 @@
use "Isar/local_defs.ML";
(*outer syntax*)
+use "Isar/keyword.ML";
use "Isar/token.ML";
-use "Isar/keyword.ML";
use "Isar/parse.ML";
use "Isar/args.ML";
--- a/src/Pure/System/options.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/System/options.scala Wed Nov 05 22:39:49 2014 +0100
@@ -93,15 +93,15 @@
{
command(SECTION) ~! text ^^
{ case _ ~ a => (options: Options) => options.set_section(a) } |
- opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
- keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
+ opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
+ $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
{ case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
(options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
}
val prefs_entry: Parser[Options => Options] =
{
- option_name ~ (keyword("=") ~! option_value) ^^
+ option_name ~ ($$$("=") ~! option_value) ^^
{ case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
}
--- a/src/Pure/Thy/thy_header.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Nov 05 22:39:49 2014 +0100
@@ -77,10 +77,17 @@
val keywordsN = "keywords";
val beginN = "begin";
-val header_lexicons =
- pairself (Scan.make_lexicon o map Symbol.explode)
- (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
- [headerN, chapterN, sectionN, subsectionN, subsubsectionN, theoryN]);
+val header_keywords =
+ Keyword.empty_keywords
+ |> fold (Keyword.add o rpair NONE)
+ ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
+ |> fold Keyword.add
+ [(headerN, SOME Keyword.heading),
+ (chapterN, SOME Keyword.heading),
+ (sectionN, SOME Keyword.heading),
+ (subsectionN, SOME Keyword.heading),
+ (subsubsectionN, SOME Keyword.heading),
+ (theoryN, SOME Keyword.thy_begin)];
(* header args *)
@@ -124,21 +131,21 @@
(* read header *)
val heading =
- (Parse.command_name headerN ||
- Parse.command_name chapterN ||
- Parse.command_name sectionN ||
- Parse.command_name subsectionN ||
- Parse.command_name subsubsectionN) --
+ (Parse.command headerN ||
+ Parse.command chapterN ||
+ Parse.command sectionN ||
+ Parse.command subsectionN ||
+ Parse.command subsubsectionN) --
Parse.tags -- Parse.!!! Parse.document_source;
val header =
- (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
+ (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
fun token_source pos str =
str
|> Source.of_string_limited 8000
|> Symbol.source
- |> Token.source_strict (K header_lexicons) pos;
+ |> Token.source_strict header_keywords pos;
fun read_source pos source =
let val res =
--- a/src/Pure/Thy/thy_header.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala Wed Nov 05 22:39:49 2014 +0100
@@ -27,9 +27,15 @@
val AND = "and"
val BEGIN = "begin"
- private val lexicon =
- Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN,
- HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)
+ private val header_keywords =
+ Keyword.Keywords.empty +
+ "%" + "(" + ")" + "," + "::" + "==" + AND + BEGIN + IMPORTS + KEYWORDS +
+ (HEADER, Keyword.HEADING) +
+ (CHAPTER, Keyword.HEADING) +
+ (SECTION, Keyword.HEADING) +
+ (SUBSECTION, Keyword.HEADING) +
+ (SUBSUBSECTION, Keyword.HEADING) +
+ (THEORY, Keyword.THY_BEGIN)
/* theory file name */
@@ -51,7 +57,7 @@
val file_name = atom("file name", _.is_name)
val opt_files =
- keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
+ $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
success(Nil)
val keyword_spec =
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
@@ -59,35 +65,35 @@
val keyword_decl =
rep1(string) ~
- opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
- opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
+ opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
+ opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
{ case xs ~ y ~ z => xs.map((_, y, z)) }
val keyword_decls =
- keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
+ keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
{ case xs ~ yss => (xs :: yss).flatten }
val file =
- keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
+ $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
file_name ^^ (x => (x, true))
val args =
theory_name ~
- (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
+ (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
- (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
+ (opt($$$(KEYWORDS) ~! keyword_decls) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
- keyword(BEGIN) ^^
+ $$$(BEGIN) ^^
{ case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
val heading =
- (keyword(HEADER) |
- keyword(CHAPTER) |
- keyword(SECTION) |
- keyword(SUBSECTION) |
- keyword(SUBSUBSECTION)) ~
+ (command(HEADER) |
+ command(CHAPTER) |
+ command(SECTION) |
+ command(SUBSECTION) |
+ command(SUBSUBSECTION)) ~
tags ~! document_source
- (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
+ (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
}
@@ -95,7 +101,7 @@
def read(reader: Reader[Char]): Thy_Header =
{
- val token = Token.Parsers.token(lexicon, _ => false)
+ val token = Token.Parsers.token(header_keywords)
val toks = new mutable.ListBuffer[Token]
@tailrec def scan_to_begin(in: Reader[Char])
@@ -121,7 +127,7 @@
/* keywords */
- type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])]
+ type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
}
@@ -138,7 +144,7 @@
val f = Symbol.decode _
Thy_Header(f(name), imports.map(f),
keywords.map({ case (a, b, c) =>
- (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
+ (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
}
}
--- a/src/Pure/Thy/thy_output.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Nov 05 22:39:49 2014 +0100
@@ -23,9 +23,9 @@
val boolean: string -> bool
val integer: string -> int
datatype markup = Markup | MarkupEnv | Verbatim
- val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
+ val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
val check_text: Symbol_Pos.source -> Toplevel.state -> unit
- val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+ val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
val pretty_text: Proof.context -> string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
@@ -158,9 +158,9 @@
(* eval_antiq *)
-fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
+fun eval_antiq keywords state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
let
- val (opts, src) = Token.read_antiq lex antiq (ss, pos);
+ val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
val print_ctxt = Context_Position.set_visible false preview_ctxt;
@@ -171,13 +171,13 @@
(* check_text *)
-fun eval_antiquote lex state (txt, pos) =
+fun eval_antiquote keywords state (txt, pos) =
let
fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
| words (Antiquote.Antiq _) = [];
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
- | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
+ | expand (Antiquote.Antiq antiq) = eval_antiq keywords state antiq;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val _ = Position.reports (maps words ants);
@@ -190,7 +190,7 @@
fun check_text {delimited, text, pos} state =
(Position.report pos (Markup.language_document delimited);
if Toplevel.is_skipped_proof state then ()
- else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos)));
+ else ignore (eval_antiquote (Keyword.get_keywords ()) state (text, pos)));
@@ -207,8 +207,8 @@
| MarkupEnvToken of string * (string * Position.T)
| VerbatimToken of string * Position.T;
-fun output_token lex state =
- let val eval = eval_antiquote lex state in
+fun output_token keywords state =
+ let val eval = eval_antiquote keywords state in
fn NoToken => ""
| BasicToken tok => Latex.output_basic tok
| MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
@@ -265,11 +265,11 @@
in
-fun present_span lex default_tags span state state'
+fun present_span keywords default_tags span state state'
(tag_stack, active_tag, newline, buffer, present_cont) =
let
val present = fold (fn (tok, (flag, 0)) =>
- Buffer.add (output_token lex state' tok)
+ Buffer.add (output_token keywords state' tok)
#> Buffer.add flag
| _ => I);
@@ -351,7 +351,7 @@
in
-fun present_thy lex default_tags is_markup command_results toks =
+fun present_thy keywords default_tags is_markup command_results toks =
let
(* tokens *)
@@ -423,7 +423,7 @@
(* present commands *)
fun present_command tr span st st' =
- Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
+ Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
fun present _ [] = I
| present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
--- a/src/Pure/Tools/build.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 05 22:39:49 2014 +0100
@@ -228,30 +228,30 @@
val session_name = atom("session name", _.is_name)
val option =
- name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
- val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
+ name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+ val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
val theories =
- (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
+ ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
((options | success(Nil)) ~ rep(theory_xname)) ^^
{ case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
val document_files =
- keyword(DOCUMENT_FILES) ~!
- ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^
+ $$$(DOCUMENT_FILES) ~!
+ (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
{ case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
command(SESSION) ~!
(session_name ~
- ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
- ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
- (keyword("=") ~!
- (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
- ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
- ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
+ ($$$("=") ~!
+ (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
+ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
rep1(theories) ~
- ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
(rep(document_files) ^^ (x => x.flatten))))) ^^
{ case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
--- a/src/Pure/Tools/find_consts.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML Wed Nov 05 22:39:49 2014 +0100
@@ -140,10 +140,12 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+
in
fun read_query pos str =
- Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+ Outer_Syntax.scan query_keywords pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/Tools/find_theorems.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Nov 05 22:39:49 2014 +0100
@@ -526,10 +526,12 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+val query_keywords = Keyword.add (":", NONE) Keyword.empty_keywords;
+
in
fun read_query pos str =
- Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+ Outer_Syntax.scan query_keywords pos str
|> filter Token.is_proper
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
|> #1;
--- a/src/Pure/Tools/rail.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Pure/Tools/rail.ML Wed Nov 05 22:39:49 2014 +0100
@@ -316,7 +316,7 @@
fun output_rules state rules =
let
- val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
+ val output_antiq = Thy_Output.eval_antiq (Keyword.get_keywords ()) state;
fun output_text b s =
Output.output s
|> b ? enclose "\\isakeyword{" "}"
--- a/src/Tools/Code/code_target.ML Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Tools/Code/code_target.ML Wed Nov 05 22:39:49 2014 +0100
@@ -695,7 +695,7 @@
let
val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
- (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none);
+ (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_keywords ()) Position.none);
in case parse cmd_expr
of SOME f => (writeln "Now generating code..."; f ctxt)
| NONE => error ("Bad directive " ^ quote cmd_expr)
--- a/src/Tools/jEdit/src/rendering.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 05 22:39:49 2014 +0100
@@ -85,7 +85,7 @@
}
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
- if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
+ if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
else if (token.is_delimiter) JEditToken.OPERATOR
else token_style(token.kind)
--- a/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 19:43:17 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 22:39:49 2014 +0100
@@ -44,6 +44,9 @@
case Some(syntax) =>
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+ def is_command_kind(token: Token, pred: String => Boolean): Boolean =
+ syntax.keywords.is_command_kind(token, pred)
+
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
filter(_.info.is_proper)
@@ -60,45 +63,45 @@
iterator(caret_line, 1).find(info => info.range.touches(caret))
match {
- case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
find_block(
- syntax.command_kind(_, Keyword.proof_goal),
- syntax.command_kind(_, Keyword.qed),
- syntax.command_kind(_, Keyword.qed_global),
+ is_command_kind(_, Keyword.proof_goal),
+ is_command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.qed_global),
t =>
- syntax.command_kind(t, Keyword.diag) ||
- syntax.command_kind(t, Keyword.proof),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof),
caret_iterator())
- case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
find_block(
- syntax.command_kind(_, Keyword.proof_goal),
- syntax.command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.proof_goal),
+ is_command_kind(_, Keyword.qed),
_ => false,
t =>
- syntax.command_kind(t, Keyword.diag) ||
- syntax.command_kind(t, Keyword.proof),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof),
caret_iterator())
- case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
- rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory))
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
+ rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
match {
case Some(Text.Info(range2, tok))
- if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
+ if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
case _ => None
}
- case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
find_block(
- syntax.command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.qed),
t =>
- syntax.command_kind(t, Keyword.proof_goal) ||
- syntax.command_kind(t, Keyword.theory_goal),
+ is_command_kind(t, Keyword.proof_goal) ||
+ is_command_kind(t, Keyword.theory_goal),
_ => false,
t =>
- syntax.command_kind(t, Keyword.diag) ||
- syntax.command_kind(t, Keyword.proof) ||
- syntax.command_kind(t, Keyword.theory_goal),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof) ||
+ is_command_kind(t, Keyword.theory_goal),
rev_caret_iterator())
case Some(Text.Info(range1, tok)) if tok.is_begin =>
@@ -114,7 +117,7 @@
find(info => info.info.is_command || info.info.is_begin)
match {
case Some(Text.Info(range3, tok)) =>
- if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3))
+ if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
else Some((range1, range2))
case None => None
}