--- a/src/Doc/antiquote_setup.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Wed Nov 05 20:20:57 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/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 05 20:20:57 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,11 @@
fun thms_of_name ctxt name =
let
- val lex = Keyword.get_lexicons
val get = maps (Proof_Context.get_fact ctxt o fst)
in
Source.of_string name
|> Symbol.source
- |> Token.source lex Position.start
+ |> Token.source Keyword.get_keywords Position.start
|> Token.source_proper
|> Source.source Token.stopper (Parse.xthms1 >> get)
|> Source.exhaust
--- a/src/HOL/Tools/try0.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Tools/try0.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/Pure/Isar/keyword.ML Wed Nov 05 20:20:57 2014 +0100
@@ -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,
+ command_kinds: T Symtab.table};
+
+fun minor_keywords (Keywords {minor, ...}) = minor;
+fun major_keywords (Keywords {major, ...}) = major;
+fun command_kinds (Keywords {command_kinds, ...}) = command_kinds;
+
+fun make_keywords (minor, major, command_kinds) =
+ Keywords {minor = minor, major = major, command_kinds = command_kinds};
-fun make_keywords (lexicons, commands) =
- Keywords {lexicons = lexicons, commands = commands};
+fun map_keywords f (Keywords {minor, major, command_kinds}) =
+ make_keywords (f (minor, major, command_kinds));
+
+val empty_keywords =
+ make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
-local
+fun merge_keywords
+ (Keywords {minor = minor1, major = major1, command_kinds = command_kinds1},
+ Keywords {minor = minor2, major = major2, command_kinds = command_kinds2}) =
+ make_keywords
+ (Scan.merge_lexicons (minor1, minor2),
+ Scan.merge_lexicons (major1, major2),
+ Symtab.merge (K true) (command_kinds1, command_kinds2));
-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, command_kinds) =>
+ (case opt_kind of
+ NONE =>
+ let
+ val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+ in (minor', major, command_kinds) end
+ | SOME kind =>
+ let
+ val major' = Scan.extend_lexicon (Symbol.explode name) major;
+ val command_kinds' = Symtab.update (name, kind) command_kinds;
+ in (minor, major', command_kinds') 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 () = command_kinds (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/outer_syntax.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Wed Nov 05 20:20:57 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;
@@ -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 (K 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 (K keywords) pos
|> commands_source syntax
|> Source.exhaust;
--- a/src/Pure/Isar/token.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Nov 05 20:20:57 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: (unit -> 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: (unit -> 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 get_keywords =
let
- val scan_strict = Scan.bulk (fn xs => scan (get_lex ()) xs);
+ val scan_strict = Scan.bulk (fn xs => scan (get_keywords ()) xs);
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 get pos src = Symbol_Pos.source pos src |> source' false get;
+fun source_strict get pos src = Symbol_Pos.source pos src |> source' true get;
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 (K (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/ML/ml_context.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/Pure/PIDE/document.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/Pure/PIDE/resources.ML Wed Nov 05 20:20:57 2014 +0100
@@ -148,8 +148,7 @@
val {name = (name, _), ...} = header;
val _ = Thy_Header.define_keywords header;
- val lexs = Keyword.get_lexicons ();
- val toks = Outer_Syntax.scan lexs text_pos text;
+ val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
val spans = Outer_Syntax.parse_spans toks;
val elements = Thy_Syntax.parse_elements spans;
@@ -165,13 +164,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 20:05:32 2014 +0100
+++ b/src/Pure/ROOT.ML Wed Nov 05 20:20:57 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/Thy/thy_header.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Nov 05 20:20:57 2014 +0100
@@ -77,10 +77,13 @@
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 o rpair (SOME Keyword.heading))
+ [headerN, chapterN, sectionN, subsectionN, subsubsectionN]
+ |> Keyword.add (theoryN, SOME Keyword.thy_begin);
(* header args *)
@@ -138,7 +141,7 @@
str
|> Source.of_string_limited 8000
|> Symbol.source
- |> Token.source_strict (K header_lexicons) pos;
+ |> Token.source_strict (K header_keywords) pos;
fun read_source pos source =
let val res =
--- a/src/Pure/Thy/thy_header.scala Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala Wed Nov 05 20:20:57 2014 +0100
@@ -27,7 +27,7 @@
val AND = "and"
val BEGIN = "begin"
- private val keywords =
+ private val header_keywords =
Keyword.Keywords(
List("%", "(", ")", ",", "::", "==", AND, BEGIN,
HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
@@ -96,7 +96,7 @@
def read(reader: Reader[Char]): Thy_Header =
{
- val token = Token.Parsers.token(keywords)
+ val token = Token.Parsers.token(header_keywords)
val toks = new mutable.ListBuffer[Token]
@tailrec def scan_to_begin(in: Reader[Char])
--- a/src/Pure/Thy/thy_output.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Nov 05 20:20:57 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/find_consts.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML Wed Nov 05 20:20:57 2014 +0100
@@ -143,7 +143,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+ Outer_Syntax.scan (Keyword.get_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 20:05:32 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Nov 05 20:20:57 2014 +0100
@@ -529,7 +529,7 @@
in
fun read_query pos str =
- Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+ Outer_Syntax.scan (Keyword.get_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 20:05:32 2014 +0100
+++ b/src/Pure/Tools/rail.ML Wed Nov 05 20:20:57 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 20:05:32 2014 +0100
+++ b/src/Tools/Code/code_target.ML Wed Nov 05 20:20:57 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)