replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
(* Title: Pure/Thy/thy_header.ML
Author: Markus Wenzel, TU Muenchen
Theory headers -- independent of outer syntax.
*)
signature THY_HEADER =
sig
val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
end;
structure Thy_Header: THY_HEADER =
struct
(* keywords *)
val headerN = "header";
val theoryN = "theory";
val importsN = "imports";
val usesN = "uses";
val beginN = "begin";
val header_lexicon = Scan.make_lexicon
(map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]);
(* header args *)
val file_name = Parse.group "file name" Parse.name;
val theory_name = Parse.group "theory name" Parse.name;
val file =
Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
file_name >> rpair true;
val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
val args =
theory_name -- (Parse.$$$ importsN |--
Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
>> Parse.triple2;
(* read header *)
val header =
(Parse.$$$ headerN -- Parse.tags) |--
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
(Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
(Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
fun read pos src =
let val res =
src
|> Symbol.source {do_recover = false}
|> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
|> Token.source_proper
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
|> Source.get_single;
in
(case res of SOME (x, _) => x
| NONE => error ("Unexpected end of input" ^ Position.str_of pos))
end;
end;