--- a/src/Doc/antiquote_setup.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Sun Nov 30 12:24:56 2014 +0100
@@ -69,7 +69,7 @@
| _ => error ("Single ML name expected in input: " ^ quote txt));
fun prep_ml source =
- (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
+ (#1 (Input.source_content source), ML_Lex.read_source false source);
fun index_ml name kind ml = Thy_Output.antiquotation name
(Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
@@ -90,7 +90,7 @@
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
- val (pos, _) = #range source1;
+ val pos = Input.pos_of source1;
val _ =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
handle ERROR msg => error (msg ^ Position.here pos);
--- a/src/HOL/ex/Cartouche_Examples.thy Sat Nov 29 14:43:10 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Sun Nov 30 12:24:56 2014 +0100
@@ -146,8 +146,7 @@
ML_Lex.read Position.none "fn _ => (" @
ML_Lex.read_source false source @
ML_Lex.read Position.none ");";
- val (pos, _) = #range source;
- val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags pos toks;
+ val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
in "" end);
*}
@@ -204,7 +203,7 @@
structure ML_Tactic:
sig
val set: (Proof.context -> tactic) -> Proof.context -> Proof.context
- val ml_tactic: Symbol_Pos.source -> Proof.context -> tactic
+ val ml_tactic: Input.source -> Proof.context -> tactic
end =
struct
structure Data = Proof_Data(type T = Proof.context -> tactic fun init _ = K no_tac);
@@ -214,7 +213,7 @@
fun ml_tactic source ctxt =
let
val ctxt' = ctxt |> Context.proof_map
- (ML_Context.expression (#range source) "tactic" "Proof.context -> tactic"
+ (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
"Context.map_proof (ML_Tactic.set tactic)"
(ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
ML_Lex.read_source false source));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/input.ML Sun Nov 30 12:24:56 2014 +0100
@@ -0,0 +1,43 @@
+(* Title: Pure/General/input.ML
+ Author: Makarius
+
+Generic input with position information.
+*)
+
+signature INPUT =
+sig
+ type source
+ val is_delimited: source -> bool
+ val text_of: source -> Symbol_Pos.text
+ val pos_of: source -> Position.T
+ val range_of: source -> Position.range
+ val source: bool -> Symbol_Pos.text -> Position.range -> source
+ val source_explode: source -> Symbol_Pos.T list
+ val source_content: source -> string * Position.T
+end;
+
+structure Input: INPUT =
+struct
+
+abstype source = Source of {delimited: bool, text: Symbol_Pos.text, range: Position.range}
+with
+
+fun is_delimited (Source {delimited, ...}) = delimited;
+fun text_of (Source {text, ...}) = text;
+fun pos_of (Source {range = (pos, _), ...}) = pos;
+fun range_of (Source {range, ...}) = range;
+
+fun source delimited text range =
+ Source {delimited = delimited, text = text, range = range};
+
+fun source_explode (Source {text, range = (pos, _), ...}) =
+ Symbol_Pos.explode (text, pos);
+
+fun source_content (Source {text, range = (pos, _), ...}) =
+ let val syms = Symbol_Pos.explode (text, pos)
+ in (Symbol_Pos.content syms, pos) end;
+
+end;
+
+end;
+
--- a/src/Pure/General/symbol_pos.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Sun Nov 30 12:24:56 2014 +0100
@@ -39,9 +39,6 @@
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, range: Position.range}
- val source_explode: source -> T list
- val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -253,16 +250,6 @@
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, range: Position.range};
-
-fun source_explode {delimited = _, text, range = (pos, _)} = explode (text, pos);
-
-fun source_content {delimited = _, text, range = (pos, _)} =
- let val syms = explode (text, pos) in (content syms, pos) end;
-
-
(* identifiers *)
local
--- a/src/Pure/Isar/args.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/args.ML Sun Nov 30 12:24:56 2014 +0100
@@ -22,11 +22,11 @@
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val cartouche_inner_syntax: string parser
- val cartouche_source_position: Symbol_Pos.source parser
- val text_source_position: Symbol_Pos.source parser
+ val cartouche_source_position: Input.source parser
+ val text_source_position: Input.source parser
val text: string parser
val name_inner_syntax: string parser
- val name_source_position: Symbol_Pos.source parser
+ val name_source_position: Input.source parser
val name: string parser
val binding: binding parser
val alt_name: string parser
@@ -46,7 +46,7 @@
val named_fact: (string -> string option * thm list) -> thm list parser
val named_attribute: (string * Position.T -> morphism -> attribute) ->
(morphism -> attribute) parser
- val text_declaration: (Symbol_Pos.source -> declaration) -> declaration parser
+ val text_declaration: (Input.source -> declaration) -> declaration parser
val typ_abbrev: typ context_parser
val typ: typ context_parser
val term: term context_parser
--- a/src/Pure/Isar/attrib.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Nov 30 12:24:56 2014 +0100
@@ -41,7 +41,7 @@
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val local_setup: Binding.binding -> attribute context_parser -> string ->
local_theory -> local_theory
- val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+ val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
val internal: (morphism -> attribute) -> Token.src
val add_del: attribute -> attribute -> attribute context_parser
@@ -49,7 +49,7 @@
val thms: thm list context_parser
val multi_thm: thm list context_parser
val check_attribs: Proof.context -> Token.src list -> Token.src list
- val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
+ val read_attribs: Proof.context -> Input.source -> Token.src list
val transform_facts: morphism ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list
@@ -208,7 +208,7 @@
fun attribute_setup name source comment =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser"
+ |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
" parser " ^ ML_Syntax.print_string comment ^ ")")
|> Context.proof_map;
@@ -287,11 +287,11 @@
fun read_attribs ctxt source =
let
val keywords = Thy_Header.get_keywords' ctxt;
- val syms = Symbol_Pos.source_explode source;
+ val syms = Input.source_explode source;
in
(case Token.read_no_commands keywords Parse.attribs syms of
[raw_srcs] => check_attribs ctxt raw_srcs
- | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
+ | _ => error ("Malformed attributes" ^ Position.here (Input.pos_of source)))
end;
--- a/src/Pure/Isar/isar_cmd.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 30 12:24:56 2014 +0100
@@ -6,20 +6,19 @@
signature ISAR_CMD =
sig
- val global_setup: Symbol_Pos.source -> theory -> theory
- val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
- val parse_ast_translation: Symbol_Pos.source -> theory -> theory
- val parse_translation: Symbol_Pos.source -> theory -> theory
- val print_translation: Symbol_Pos.source -> theory -> theory
- val typed_print_translation: Symbol_Pos.source -> theory -> theory
- val print_ast_translation: Symbol_Pos.source -> theory -> theory
+ val global_setup: Input.source -> theory -> theory
+ val local_setup: Input.source -> Proof.context -> Proof.context
+ val parse_ast_translation: Input.source -> theory -> theory
+ val parse_translation: Input.source -> theory -> theory
+ val print_translation: Input.source -> theory -> theory
+ val typed_print_translation: Input.source -> theory -> theory
+ val print_ast_translation: Input.source -> theory -> theory
val translations: (xstring * string) Syntax.trrule list -> theory -> theory
val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
- val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
+ val oracle: bstring * Position.range -> Input.source -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
- val declaration: {syntax: bool, pervasive: bool} ->
- Symbol_Pos.source -> local_theory -> local_theory
- val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
+ val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
+ val simproc_setup: string * Position.T -> string list -> Input.source ->
string list -> local_theory -> local_theory
val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -32,7 +31,7 @@
val immediate_proof: Toplevel.transition -> Toplevel.transition
val done_proof: Toplevel.transition -> Toplevel.transition
val skip_proof: Toplevel.transition -> Toplevel.transition
- val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
+ val ml_diag: bool -> Input.source -> Toplevel.transition -> Toplevel.transition
val diag_state: Proof.context -> Toplevel.state
val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
@@ -60,13 +59,13 @@
fun global_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "setup" "theory -> theory"
+ |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
"Context.map_theory setup"
|> Context.theory_map;
fun local_setup source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
+ |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
"Context.map_proof local_setup"
|> Context.proof_map;
@@ -75,35 +74,35 @@
fun parse_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "parse_ast_translation"
+ |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
fun parse_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "parse_translation"
+ |> ML_Context.expression (Input.range_of source) "parse_translation"
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
fun print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "print_translation"
+ |> ML_Context.expression (Input.range_of source) "print_translation"
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
fun typed_print_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "typed_print_translation"
+ |> ML_Context.expression (Input.range_of source) "typed_print_translation"
"(string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
fun print_ast_translation source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "print_ast_translation"
+ |> ML_Context.expression (Input.range_of source) "print_ast_translation"
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
|> Context.theory_map;
@@ -129,7 +128,7 @@
fun oracle (name, range) source =
let
- val body_range = #range source;
+ val body_range = Input.range_of source;
val body = ML_Lex.read_source false source;
val hidden = ML_Lex.read Position.none;
@@ -164,7 +163,7 @@
fun declaration {syntax, pervasive} source =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
+ |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
|> Context.proof_map;
@@ -174,7 +173,7 @@
fun simproc_setup name lhss source identifier =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "proc"
+ |> ML_Context.expression (Input.range_of source) "proc"
"Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
\lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
--- a/src/Pure/Isar/isar_syn.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Nov 30 12:24:56 2014 +0100
@@ -208,7 +208,7 @@
(Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
let
val ([{lines, pos, ...}], thy') = files thy;
- val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
+ val source = Input.source true (cat_lines lines) (pos, pos);
val flags = {SML = true, exchange = false, redirect = true, verbose = true};
in
thy' |> Context.theory_map
--- a/src/Pure/Isar/method.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/method.ML Sun Nov 30 12:24:56 2014 +0100
@@ -61,8 +61,7 @@
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
local_theory -> local_theory
- val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
- local_theory -> local_theory
+ val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory
val method: Proof.context -> Token.src -> Proof.context -> method
val method_closure: Proof.context -> Token.src -> Token.src
val method_cmd: Proof.context -> Token.src -> Proof.context -> method
@@ -282,7 +281,7 @@
Scan.lift (Args.text_declaration (fn source =>
let
val context' = context |>
- ML_Context.expression (#range source)
+ ML_Context.expression (Input.range_of source)
"tactic" "Morphism.morphism -> thm list -> tactic"
"Method.set_tactic tactic"
(ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
@@ -381,7 +380,7 @@
fun method_setup name source comment =
ML_Lex.read_source false source
- |> ML_Context.expression (#range source) "parser"
+ |> ML_Context.expression (Input.range_of source) "parser"
"(Proof.context -> Proof.method) context_parser"
("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
" parser " ^ ML_Syntax.print_string comment ^ ")")
--- a/src/Pure/Isar/parse.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/parse.ML Sun Nov 30 12:24:56 2014 +0100
@@ -16,7 +16,7 @@
val token: 'a parser -> Token.T parser
val range: 'a parser -> ('a * Position.range) parser
val position: 'a parser -> ('a * Position.T) parser
- val source_position: 'a parser -> Symbol_Pos.source parser
+ val source_position: 'a parser -> Input.source parser
val inner_syntax: 'a parser -> string parser
val command_: string parser
val keyword: string parser
@@ -92,8 +92,8 @@
val simple_fixes: (binding * string option) list parser
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
- val ML_source: Symbol_Pos.source parser
- val document_source: Symbol_Pos.source parser
+ val ML_source: Input.source parser
+ val document_source: Input.source parser
val term_group: string parser
val prop_group: string parser
val term: string parser
--- a/src/Pure/Isar/proof_context.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Nov 30 12:24:56 2014 +0100
@@ -403,7 +403,7 @@
fun read_class ctxt text =
let
- val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text));
+ val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
val _ = Position.reports reports;
in c end;
@@ -471,7 +471,7 @@
fun read_type_name ctxt flags text =
let
val (T, reports) =
- check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+ check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
val _ = Position.reports reports;
in T end;
@@ -519,7 +519,7 @@
fun read_const ctxt flags text =
let
- val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+ val (xname, pos) = Input.source_content (Syntax.read_token text);
val (t, reports) = check_const ctxt flags (xname, [pos]);
val _ = Position.reports reports;
in t end;
--- a/src/Pure/Isar/token.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/token.ML Sun Nov 30 12:24:56 2014 +0100
@@ -52,7 +52,7 @@
val is_blank: T -> bool
val is_newline: T -> bool
val inner_syntax_of: T -> string
- val source_position_of: T -> Symbol_Pos.source
+ val source_position_of: T -> Input.source
val content_of: T -> string
val keyword_markup: bool * Markup.T -> string -> Markup.T
val completion_report: T -> Position.report_text list
@@ -269,7 +269,7 @@
in YXML.string_of tree end;
fun source_position_of (Token ((source, range), (kind, _), _)) =
- {delimited = delimited_kind kind, text = source, range = range};
+ Input.source (delimited_kind kind) source range;
fun content_of (Token (_, (_, x), _)) = x;
--- a/src/Pure/ML/ml_antiquotations.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sun Nov 30 12:24:56 2014 +0100
@@ -34,10 +34,10 @@
val _ = Theory.setup
(ML_Antiquotation.value @{binding source}
- (Scan.lift Args.text_source_position >> (fn {delimited, text, range} =>
- "{delimited = " ^ Bool.toString delimited ^
- ", text = " ^ ML_Syntax.print_string text ^
- ", range = " ^ ML_Syntax.print_range range ^ "}")));
+ (Scan.lift Args.text_source_position >> (fn source =>
+ "Input.source " ^ Bool.toString (Input.is_delimited source) ^ " " ^
+ ML_Syntax.print_string (Input.text_of source) ^ " " ^
+ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
(* formal entities *)
--- a/src/Pure/ML/ml_context.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Sun Nov 30 12:24:56 2014 +0100
@@ -21,10 +21,10 @@
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
val eval_file: ML_Compiler.flags -> Path.T -> unit
- val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
+ val eval_source: ML_Compiler.flags -> Input.source -> unit
val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
- val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
+ val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
val expression: Position.range -> string -> string -> string ->
ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
end
@@ -173,7 +173,7 @@
in eval flags pos (ML_Lex.read pos (File.read path)) end;
fun eval_source flags source =
- eval flags (#1 (#range source)) (ML_Lex.read_source (#SML flags) source);
+ eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
fun eval_in ctxt flags pos ants =
Context.setmp_thread_data (Option.map Context.Proof ctxt)
--- a/src/Pure/ML/ml_file.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_file.ML Sun Nov 30 12:24:56 2014 +0100
@@ -13,7 +13,7 @@
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
- val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
+ val source = Input.source true (cat_lines lines) (pos, pos);
val flags = {SML = false, exchange = false, redirect = true, verbose = true};
in
gthy
--- a/src/Pure/ML/ml_lex.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Sun Nov 30 12:24:56 2014 +0100
@@ -27,7 +27,7 @@
val tokenize: string -> token list
val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
- val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
+ val read_source: bool -> Input.source -> token Antiquote.antiquote list
end;
structure ML_Lex: ML_LEX =
@@ -330,13 +330,15 @@
read Position.none
#> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
-fun read_source SML ({delimited, text, range = (pos, _)}: Symbol_Pos.source) =
+fun read_source SML source =
let
+ val pos = Input.pos_of source;
val language = if SML then Markup.language_SML else Markup.language_ML;
val _ =
- if Position.is_reported_range pos then Position.report pos (language delimited)
+ if Position.is_reported_range pos
+ then Position.report pos (language (Input.is_delimited source))
else ();
- in gen_read SML pos text end;
+ in gen_read SML pos (Input.text_of source) end;
end;
--- a/src/Pure/ROOT Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT Sun Nov 30 12:24:56 2014 +0100
@@ -81,6 +81,7 @@
"General/graph.ML"
"General/graph_display.ML"
"General/heap.ML"
+ "General/input.ML"
"General/integer.ML"
"General/linear_set.ML"
"General/long_name.ML"
--- a/src/Pure/ROOT.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT.ML Sun Nov 30 12:24:56 2014 +0100
@@ -32,6 +32,7 @@
use "General/symbol.ML";
use "General/position.ML";
use "General/symbol_pos.ML";
+use "General/input.ML";
use "General/antiquote.ML";
use "ML/ml_lex.ML";
use "ML/ml_parse.ML";
--- a/src/Pure/Syntax/syntax.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Nov 30 12:24:56 2014 +0100
@@ -15,7 +15,7 @@
val ambiguity_limit_raw: Config.raw
val ambiguity_limit: int Config.T
val read_token_pos: string -> Position.T
- val read_token: string -> Symbol_Pos.source
+ val read_token: string -> Input.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
@@ -169,11 +169,11 @@
else (false, Position.no_range)
| token_range (XML.Text _) = (false, Position.no_range);
-fun token_source tree : Symbol_Pos.source =
+fun token_source tree : Input.source =
let
val text = XML.content_of [tree];
val (delimited, range) = token_range tree;
- in {delimited = delimited, text = text, range = range} end;
+ in Input.source delimited text range end;
in
@@ -186,9 +186,9 @@
fun parse_tree tree =
let
val source = token_source tree;
- val syms = Symbol_Pos.source_explode source;
- val (pos, _) = #range source;
- val _ = Context_Position.report ctxt pos (markup (#delimited source));
+ val syms = Input.source_explode source;
+ val pos = Input.pos_of source;
+ val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
in parse (syms, pos) end;
in
(case YXML.parse_body str handle Fail msg => error msg of
--- a/src/Pure/Syntax/syntax_phases.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Nov 30 12:24:56 2014 +0100
@@ -462,8 +462,8 @@
| decode ps (Ast.Appl asts) = decode_appl ps asts;
val source = Syntax.read_token str;
- val (pos, _) = #range source;
- val syms = Symbol_Pos.source_explode source;
+ val pos = Input.pos_of source;
+ val syms = Input.source_explode source;
val ast =
parse_asts ctxt true root (syms, pos)
|> uncurry (report_result ctxt pos)
--- a/src/Pure/Thy/latex.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 30 12:24:56 2014 +0100
@@ -132,8 +132,8 @@
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
else if Token.is_kind Token.Verbatim tok then
let
- val {text, range = (pos, _), ...} = Token.source_position_of tok;
- val ants = Antiquote.read (Symbol_Pos.explode (text, pos), pos);
+ val source = Token.source_position_of tok;
+ val ants = Antiquote.read (Input.source_explode source, Input.pos_of source);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else if Token.is_kind Token.Cartouche tok then
--- a/src/Pure/Thy/thy_output.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Nov 30 12:24:56 2014 +0100
@@ -23,7 +23,7 @@
val boolean: string -> bool
val integer: string -> int
val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
- val check_text: Symbol_Pos.source -> Toplevel.state -> unit
+ val check_text: Input.source -> Toplevel.state -> unit
val present_thy: theory -> (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
@@ -33,8 +33,8 @@
Token.src -> 'a list -> Pretty.T list
val output: Proof.context -> Pretty.T list -> string
val verbatim_text: Proof.context -> string -> string
- val old_header_command: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
- val document_command: (xstring * Position.T) option * Symbol_Pos.source ->
+ val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
+ val document_command: (xstring * Position.T) option * Input.source ->
Toplevel.transition -> Toplevel.transition
end;
@@ -192,10 +192,10 @@
val _ = Position.reports (maps words ants);
in implode (map expand ants) end;
-fun check_text ({delimited, text, range}: Symbol_Pos.source) state =
- (Position.report (fst range) (Markup.language_document delimited);
+fun check_text source state =
+ (Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
if Toplevel.is_skipped_proof state then ()
- else ignore (eval_antiquote state (text, fst range)));
+ else ignore (eval_antiquote state (Input.text_of source, Input.pos_of source)));
@@ -377,8 +377,11 @@
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
Scan.repeat tag --
Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
- >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
- let val name = Token.content_of tok
+ >> (fn (((tok, pos'), tags), source) =>
+ let
+ val name = Token.content_of tok;
+ val text = Input.text_of source;
+ val pos = Input.pos_of source;
in (SOME (name, pos', tags), (mk (name, (text, pos)), (flag, d))) end));
val command = Scan.peek (fn d =>
@@ -389,8 +392,8 @@
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
- Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source)
- >> (fn {text, range = (pos, _), ...} => (NONE, (MarkupToken ("cmt", (text, pos)), ("", d)))));
+ Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >> (fn source =>
+ (NONE, (MarkupToken ("cmt", (Input.text_of source, Input.pos_of source)), ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
@@ -487,9 +490,8 @@
fun pretty_text_report ctxt source =
let
- val {delimited, range = (pos, _), ...} = source;
- val _ = Context_Position.report ctxt pos (Markup.language_text delimited);
- val (s, _) = Symbol_Pos.source_content source;
+ val (s, pos) = Input.source_content source;
+ val _ = Context_Position.report ctxt pos (Markup.language_text (Input.is_delimited source));
in pretty_text ctxt s end;
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
@@ -669,8 +671,8 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
(fn {context = ctxt, ...} => fn source =>
- (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#1 (#range source)) (ml source);
- Symbol_Pos.source_content source |> #1
+ (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
+ Input.source_content source |> #1
|> verbatim_text ctxt));
fun ml_enclose bg en source =
@@ -690,7 +692,7 @@
ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
(fn source =>
ML_Lex.read Position.none ("ML_Env.check_functor " ^
- ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
+ ML_Syntax.print_string (#1 (Input.source_content source)))) #>
ml_text @{binding ML_text} (K []));
--- a/src/Pure/Thy/thy_syntax.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sun Nov 30 12:24:56 2014 +0100
@@ -26,9 +26,8 @@
fun reports_of_token tok =
let
- val {text, range = (pos, _), ...} = Token.source_position_of tok;
val malformed_symbols =
- Symbol_Pos.explode (text, pos)
+ Input.source_explode (Token.source_position_of tok)
|> map_filter (fn (sym, pos) =>
if Symbol.is_malformed sym
then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
--- a/src/Pure/Tools/rail.ML Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Tools/rail.ML Sun Nov 30 12:24:56 2014 +0100
@@ -281,11 +281,10 @@
(* read *)
-fun read ctxt (source: Symbol_Pos.source) =
+fun read ctxt source =
let
- val {text, range = (pos, _), ...} = source;
- val _ = Context_Position.report ctxt pos Markup.language_rail;
- val toks = tokenize (Symbol_Pos.explode (text, pos));
+ val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
+ val toks = tokenize (Input.source_explode source);
val _ = Context_Position.reports ctxt (maps reports_of_token toks);
val rules = parse_rules toks;
val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);