--- a/src/Pure/General/symbol_pos.ML Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sat Mar 01 23:17:37 2014 +0100
@@ -37,10 +37,11 @@
val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
(T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
type text = string
- type source = {delimited: bool, text: text, pos: Position.T}
val implode: T list -> text
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
+ type source = {delimited: bool, text: text, pos: Position.T}
+ val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -233,7 +234,6 @@
(* compact representation -- with Symbol.DEL padding *)
type text = string;
-type source = {delimited: bool, text: text, pos: Position.T}
fun pad [] = []
| pad [(s, _)] = [s]
@@ -257,6 +257,14 @@
in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
+(* full source information *)
+
+type source = {delimited: bool, text: text, pos: Position.T};
+
+fun source_content {delimited = _, text, pos} =
+ let val syms = explode (text, pos) in (content syms, pos) end;
+
+
(* identifiers *)
local
--- a/src/Pure/Isar/proof_context.ML Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 01 23:17:37 2014 +0100
@@ -377,9 +377,8 @@
fun read_class ctxt text =
let
val tsig = tsig_of ctxt;
- val {text, pos, ...} = Syntax.read_token_source text;
- val syms = Symbol_Pos.explode (text, pos);
- val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
+ val (s, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+ val c = Type.cert_class tsig (Type.intern_class tsig s)
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
in c end;
@@ -460,7 +459,7 @@
fun read_type_name ctxt strict text =
let
val tsig = tsig_of ctxt;
- val (c, pos) = Syntax.read_token_content text;
+ val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
in
if Lexicon.is_tid c then
(Context_Position.report ctxt pos Markup.tfree;
@@ -486,11 +485,11 @@
fun read_const_proper ctxt strict =
- prep_const_proper ctxt strict o Syntax.read_token_content;
+ prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
fun read_const ctxt strict ty text =
let
- val (c, pos) = Syntax.read_token_content text;
+ val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
val _ = no_skolem false c;
in
(case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
--- a/src/Pure/Syntax/syntax.ML Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML Sat Mar 01 23:17:37 2014 +0100
@@ -15,8 +15,7 @@
val ambiguity_limit_raw: Config.raw
val ambiguity_limit: int Config.T
val read_token_pos: string -> Position.T
- val read_token_source: string -> Symbol_Pos.source
- val read_token_content: string -> string * Position.T
+ val read_token: string -> Symbol_Pos.source
val parse_token: Proof.context -> (XML.tree list -> 'a) ->
(bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
val parse_sort: Proof.context -> string -> sort
@@ -178,13 +177,7 @@
fun read_token_pos str = #2 (token_position (YXML.parse str handle Fail msg => error msg));
-fun read_token_source str = token_source (YXML.parse str handle Fail msg => error msg);
-
-fun read_token_content str =
- let
- val {text, pos, ...} = read_token_source str;
- val syms = Symbol_Pos.explode (text, pos);
- in (Symbol_Pos.content syms, pos) end;
+fun read_token str = token_source (YXML.parse str handle Fail msg => error msg);
fun parse_token ctxt decode markup parse str =
let
--- a/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Mar 01 23:17:37 2014 +0100
@@ -440,7 +440,7 @@
else decode_appl ps asts
| decode ps (Ast.Appl asts) = decode_appl ps asts;
- val {text, pos, ...} = Syntax.read_token_source str;
+ val {text, pos, ...} = Syntax.read_token str;
val syms = Symbol_Pos.explode (text, pos);
val ast =
parse_asts ctxt true root (syms, pos)
--- a/src/Pure/Thy/thy_output.ML Sat Mar 01 22:46:31 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Mar 01 23:17:37 2014 +0100
@@ -467,10 +467,11 @@
fun pretty_text ctxt =
Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
-fun pretty_text_report ctxt {delimited, text, pos} =
+fun pretty_text_report ctxt source =
let
+ val {delimited, pos, ...} = source;
val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
- val s = Symbol_Pos.content (Symbol_Pos.explode (text, pos));
+ val (s, _) = Symbol_Pos.source_content source;
in pretty_text ctxt s end;
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -641,9 +642,10 @@
local
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
- (fn {context, ...} => fn source as {text, pos, ...} =>
- (ML_Context.eval_in (SOME context) false pos (ml source);
- Symbol_Pos.content (Symbol_Pos.explode (text, pos))
+ (fn {context, ...} => fn source =>
+ (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
+ Symbol_Pos.source_content source
+ |> #1
|> (if Config.get context quotes then quote else I)
|> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else verb_text)));
@@ -663,9 +665,9 @@
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
- (fn {text, pos, ...} =>
+ (fn source =>
ML_Lex.read Position.none ("ML_Env.check_functor " ^
- ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (text, pos))))) #>
+ ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
ml_text (Binding.name "ML_text") (K []));