1.1 --- a/NEWS Thu Mar 19 01:29:19 2009 -0700
1.2 +++ b/NEWS Thu Mar 19 11:51:49 2009 +0100
1.3 @@ -176,30 +176,28 @@
1.4 * The 'axiomatization' command now only works within a global theory
1.5 context. INCOMPATIBILITY.
1.6
1.7 -* New find_theorems criterion "solves" matching theorems that directly
1.8 -solve the current goal. Try "find_theorems solves".
1.9 -
1.10 -* Added an auto solve option, which can be enabled through the
1.11 -ProofGeneral Isabelle settings menu (disabled by default).
1.12 -
1.13 -When enabled, find_theorems solves is called whenever a new lemma is
1.14 -stated. Any theorems that could solve the lemma directly are listed
1.15 -underneath the goal.
1.16 -
1.17 -* New command 'find_consts' searches for constants based on type and
1.18 -name patterns, e.g.
1.19 +* New 'find_theorems' criterion "solves" matching theorems that
1.20 +directly solve the current goal.
1.21 +
1.22 +* Auto solve feature for main theorem statements (cf. option in Proof
1.23 +General Isabelle settings menu, enabled by default). Whenever a new
1.24 +goal is stated, "find_theorems solves" is called; any theorems that
1.25 +could solve the lemma directly are listed underneath the goal.
1.26 +
1.27 +* Command 'find_consts' searches for constants based on type and name
1.28 +patterns, e.g.
1.29
1.30 find_consts "_ => bool"
1.31
1.32 By default, matching is against subtypes, but it may be restricted to
1.33 -the whole type. Searching by name is possible. Multiple queries are
1.34 +the whole type. Searching by name is possible. Multiple queries are
1.35 conjunctive and queries may be negated by prefixing them with a
1.36 hyphen:
1.37
1.38 find_consts strict: "_ => bool" name: "Int" -"int => int"
1.39
1.40 -* New command 'local_setup' is similar to 'setup', but operates on a
1.41 -local theory context.
1.42 +* Command 'local_setup' is similar to 'setup', but operates on a local
1.43 +theory context.
1.44
1.45
1.46 *** Document preparation ***
2.1 --- a/src/Pure/General/symbol_pos.ML Thu Mar 19 01:29:19 2009 -0700
2.2 +++ b/src/Pure/General/symbol_pos.ML Thu Mar 19 11:51:49 2009 +0100
2.3 @@ -34,7 +34,7 @@
2.4 val explode: text * Position.T -> T list
2.5 end;
2.6
2.7 -structure SymbolPos: SYMBOL_POS =
2.8 +structure Symbol_Pos: SYMBOL_POS =
2.9 struct
2.10
2.11 (* type T *)
2.12 @@ -149,5 +149,5 @@
2.13
2.14 end;
2.15
2.16 -structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos; (*not open by default*)
2.17 +structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos; (*not open by default*)
2.18
3.1 --- a/src/Pure/Isar/antiquote.ML Thu Mar 19 01:29:19 2009 -0700
3.2 +++ b/src/Pure/Isar/antiquote.ML Thu Mar 19 11:51:49 2009 +0100
3.3 @@ -7,12 +7,12 @@
3.4 signature ANTIQUOTE =
3.5 sig
3.6 datatype antiquote =
3.7 - Text of string | Antiq of SymbolPos.T list * Position.T |
3.8 + Text of string | Antiq of Symbol_Pos.T list * Position.T |
3.9 Open of Position.T | Close of Position.T
3.10 val is_antiq: antiquote -> bool
3.11 - val read: SymbolPos.T list * Position.T -> antiquote list
3.12 + val read: Symbol_Pos.T list * Position.T -> antiquote list
3.13 val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
3.14 - SymbolPos.T list * Position.T -> 'a
3.15 + Symbol_Pos.T list * Position.T -> 'a
3.16 end;
3.17
3.18 structure Antiquote: ANTIQUOTE =
3.19 @@ -22,7 +22,7 @@
3.20
3.21 datatype antiquote =
3.22 Text of string |
3.23 - Antiq of SymbolPos.T list * Position.T |
3.24 + Antiq of Symbol_Pos.T list * Position.T |
3.25 Open of Position.T |
3.26 Close of Position.T;
3.27
3.28 @@ -48,7 +48,7 @@
3.29
3.30 (* scan_antiquote *)
3.31
3.32 -open BasicSymbolPos;
3.33 +open Basic_Symbol_Pos;
3.34 structure T = OuterLex;
3.35
3.36 local
3.37 @@ -63,18 +63,18 @@
3.38 Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
3.39
3.40 val scan_antiq =
3.41 - SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
3.42 + Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
3.43 T.!!! "missing closing brace of antiquotation"
3.44 - (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
3.45 + (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
3.46 >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
3.47
3.48 in
3.49
3.50 val scan_antiquote =
3.51 - (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
3.52 + (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
3.53 scan_antiq ||
3.54 - SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
3.55 - SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
3.56 + Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
3.57 + Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
3.58
3.59 end;
3.60
3.61 @@ -86,7 +86,7 @@
3.62
3.63 fun read ([], _) = []
3.64 | read (syms, pos) =
3.65 - (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
3.66 + (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
3.67 SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
3.68 | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
3.69
3.70 @@ -96,7 +96,7 @@
3.71 fun read_antiq lex scan (syms, pos) =
3.72 let
3.73 fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
3.74 - "@{" ^ SymbolPos.content syms ^ "}");
3.75 + "@{" ^ Symbol_Pos.content syms ^ "}");
3.76
3.77 val res =
3.78 Source.of_list syms
4.1 --- a/src/Pure/Isar/args.ML Thu Mar 19 01:29:19 2009 -0700
4.2 +++ b/src/Pure/Isar/args.ML Thu Mar 19 11:51:49 2009 +0100
4.3 @@ -32,7 +32,7 @@
4.4 val mode: string -> bool context_parser
4.5 val maybe: 'a parser -> 'a option parser
4.6 val name_source: string parser
4.7 - val name_source_position: (SymbolPos.text * Position.T) parser
4.8 + val name_source_position: (Symbol_Pos.text * Position.T) parser
4.9 val name: string parser
4.10 val binding: binding parser
4.11 val alt_name: string parser
5.1 --- a/src/Pure/Isar/attrib.ML Thu Mar 19 01:29:19 2009 -0700
5.2 +++ b/src/Pure/Isar/attrib.ML Thu Mar 19 11:51:49 2009 +0100
5.3 @@ -26,7 +26,8 @@
5.4 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
5.5 val syntax: attribute context_parser -> src -> attribute
5.6 val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
5.7 - val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
5.8 + val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
5.9 + theory -> theory
5.10 val no_args: attribute -> src -> attribute
5.11 val add_del: attribute -> attribute -> attribute context_parser
5.12 val add_del_args: attribute -> attribute -> src -> attribute
6.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Mar 19 01:29:19 2009 -0700
6.2 +++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 19 11:51:49 2009 +0100
6.3 @@ -6,18 +6,18 @@
6.4
6.5 signature ISAR_CMD =
6.6 sig
6.7 - val global_setup: string * Position.T -> theory -> theory
6.8 - val local_setup: string * Position.T -> Proof.context -> Proof.context
6.9 - val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
6.10 - val parse_translation: bool * (string * Position.T) -> theory -> theory
6.11 - val print_translation: bool * (string * Position.T) -> theory -> theory
6.12 - val typed_print_translation: bool * (string * Position.T) -> theory -> theory
6.13 - val print_ast_translation: bool * (string * Position.T) -> theory -> theory
6.14 - val oracle: bstring * Position.T -> SymbolPos.text * Position.T -> theory -> theory
6.15 + val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
6.16 + val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
6.17 + val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
6.18 + val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
6.19 + val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
6.20 + val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
6.21 + val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
6.22 + val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
6.23 val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
6.24 val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
6.25 - val declaration: string * Position.T -> local_theory -> local_theory
6.26 - val simproc_setup: string -> string list -> string * Position.T -> string list ->
6.27 + val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
6.28 + val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
6.29 local_theory -> local_theory
6.30 val hide_names: bool -> string * xstring list -> theory -> theory
6.31 val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
6.32 @@ -38,7 +38,7 @@
6.33 val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
6.34 val disable_pr: Toplevel.transition -> Toplevel.transition
6.35 val enable_pr: Toplevel.transition -> Toplevel.transition
6.36 - val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
6.37 + val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
6.38 val cd: Path.T -> Toplevel.transition -> Toplevel.transition
6.39 val pwd: Toplevel.transition -> Toplevel.transition
6.40 val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
6.41 @@ -75,10 +75,10 @@
6.42 val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
6.43 val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
6.44 val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
6.45 - val header_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
6.46 - val local_theory_markup: xstring option * (SymbolPos.text * Position.T) ->
6.47 + val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
6.48 + val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
6.49 Toplevel.transition -> Toplevel.transition
6.50 - val proof_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
6.51 + val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
6.52 end;
6.53
6.54 structure IsarCmd: ISAR_CMD =
6.55 @@ -152,7 +152,7 @@
6.56
6.57 fun oracle (name, pos) (body_txt, body_pos) =
6.58 let
6.59 - val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
6.60 + val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));
6.61 val txt =
6.62 "local\n\
6.63 \ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
7.1 --- a/src/Pure/Isar/isar_syn.ML Thu Mar 19 01:29:19 2009 -0700
7.2 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 19 11:51:49 2009 +0100
7.3 @@ -272,7 +272,7 @@
7.4 OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
7.5
7.6 val _ =
7.7 - OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
7.8 + OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
7.9 (P.and_list1 SpecParse.xthms1
7.10 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
7.11
7.12 @@ -295,28 +295,35 @@
7.13
7.14 (* use ML text *)
7.15
7.16 -val _ =
7.17 - OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl)
7.18 - (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
7.19 +fun inherit_env (context as Context.Proof lthy) =
7.20 + Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
7.21 + | inherit_env context = context;
7.22 +
7.23 +fun inherit_env_prf prf = Proof.map_contexts
7.24 + (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
7.25
7.26 val _ =
7.27 - OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl)
7.28 - (P.ML_source >> (fn (txt, pos) =>
7.29 - Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
7.30 + OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
7.31 + (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
7.32
7.33 val _ =
7.34 - OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl)
7.35 + OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
7.36 + (P.ML_source >> (fn (txt, pos) =>
7.37 + Toplevel.generic_theory
7.38 + (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
7.39 +
7.40 +val _ =
7.41 + OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
7.42 (P.ML_source >> (fn (txt, pos) =>
7.43 Toplevel.proof (Proof.map_context (Context.proof_map
7.44 - (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #>
7.45 - (fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf))));
7.46 + (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
7.47
7.48 val _ =
7.49 - OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
7.50 + OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
7.51 (P.ML_source >> IsarCmd.ml_diag true);
7.52
7.53 val _ =
7.54 - OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
7.55 + OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
7.56 (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
7.57
7.58 val _ =
8.1 --- a/src/Pure/Isar/local_theory.ML Thu Mar 19 01:29:19 2009 -0700
8.2 +++ b/src/Pure/Isar/local_theory.ML Thu Mar 19 11:51:49 2009 +0100
8.3 @@ -23,6 +23,7 @@
8.4 val theory: (theory -> theory) -> local_theory -> local_theory
8.5 val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
8.6 val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
8.7 + val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
8.8 val affirm: local_theory -> local_theory
8.9 val pretty: local_theory -> Pretty.T list
8.10 val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
8.11 @@ -163,6 +164,11 @@
8.12
8.13 fun target f = #2 o target_result (f #> pair ());
8.14
8.15 +fun map_contexts f =
8.16 + theory (Context.theory_map f) #>
8.17 + target (Context.proof_map f) #>
8.18 + Context.proof_map f;
8.19 +
8.20
8.21 (* basic operations *)
8.22
9.1 --- a/src/Pure/Isar/method.ML Thu Mar 19 01:29:19 2009 -0700
9.2 +++ b/src/Pure/Isar/method.ML Thu Mar 19 11:51:49 2009 +0100
9.3 @@ -81,7 +81,8 @@
9.4 -> theory -> theory
9.5 val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
9.6 val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
9.7 - val method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
9.8 + val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
9.9 + theory -> theory
9.10 val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
9.11 val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
9.12 val no_args: method -> src -> Proof.context -> method
10.1 --- a/src/Pure/Isar/outer_lex.ML Thu Mar 19 01:29:19 2009 -0700
10.2 +++ b/src/Pure/Isar/outer_lex.ML Thu Mar 19 11:51:49 2009 +0100
10.3 @@ -35,7 +35,7 @@
10.4 val is_blank: token -> bool
10.5 val is_newline: token -> bool
10.6 val source_of: token -> string
10.7 - val source_position_of: token -> SymbolPos.text * Position.T
10.8 + val source_position_of: token -> Symbol_Pos.text * Position.T
10.9 val content_of: token -> string
10.10 val unparse: token -> string
10.11 val text_of: token -> string * string
10.12 @@ -50,14 +50,14 @@
10.13 val assign: value option -> token -> unit
10.14 val closure: token -> token
10.15 val ident_or_symbolic: string -> bool
10.16 - val !!! : string -> (SymbolPos.T list -> 'a) -> SymbolPos.T list -> 'a
10.17 - val scan_quoted: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
10.18 + val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
10.19 + val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
10.20 val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
10.21 val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
10.22 - (SymbolPos.T, 'a) Source.source -> (token, (SymbolPos.T, 'a) Source.source) Source.source
10.23 + (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
10.24 val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
10.25 Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
10.26 - (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
10.27 + (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
10.28 end;
10.29
10.30 structure OuterLex: OUTER_LEX =
10.31 @@ -92,7 +92,7 @@
10.32 Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
10.33 Malformed | Error of string | Sync | EOF;
10.34
10.35 -datatype token = Token of (SymbolPos.text * Position.range) * (token_kind * string) * slot;
10.36 +datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
10.37
10.38 val str_of_kind =
10.39 fn Command => "command"
10.40 @@ -259,9 +259,9 @@
10.41
10.42 (** scanners **)
10.43
10.44 -open BasicSymbolPos;
10.45 +open Basic_Symbol_Pos;
10.46
10.47 -fun !!! msg = SymbolPos.!!! ("Outer lexical error: " ^ msg);
10.48 +fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
10.49
10.50 fun change_prompt scan = Scan.prompt "# " scan;
10.51
10.52 @@ -303,8 +303,8 @@
10.53 Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
10.54
10.55 fun scan_strs q =
10.56 - (SymbolPos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
10.57 - (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- SymbolPos.scan_pos)));
10.58 + (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
10.59 + (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos)));
10.60
10.61 in
10.62
10.63 @@ -323,8 +323,8 @@
10.64 Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
10.65
10.66 val scan_verbatim =
10.67 - (SymbolPos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
10.68 - (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- SymbolPos.scan_pos)));
10.69 + (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
10.70 + (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
10.71
10.72
10.73 (* scan space *)
10.74 @@ -339,7 +339,7 @@
10.75 (* scan comment *)
10.76
10.77 val scan_comment =
10.78 - SymbolPos.scan_pos -- (SymbolPos.scan_comment_body !!! -- SymbolPos.scan_pos);
10.79 + Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
10.80
10.81
10.82 (* scan malformed symbols *)
10.83 @@ -360,10 +360,10 @@
10.84 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
10.85
10.86 fun token k ss =
10.87 - Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.untabify_content ss), Slot);
10.88 + Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
10.89
10.90 fun token_range k (pos1, (ss, pos2)) =
10.91 - Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.untabify_content ss), Slot);
10.92 + Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
10.93
10.94 fun scan (lex1, lex2) = !!! "bad input"
10.95 (scan_string >> token_range String ||
10.96 @@ -392,11 +392,11 @@
10.97 in
10.98
10.99 fun source' {do_recover} get_lex =
10.100 - Source.source SymbolPos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
10.101 + Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
10.102 (Option.map (rpair recover) do_recover);
10.103
10.104 fun source do_recover get_lex pos src =
10.105 - SymbolPos.source pos src
10.106 + Symbol_Pos.source pos src
10.107 |> source' do_recover get_lex;
10.108
10.109 end;
11.1 --- a/src/Pure/Isar/outer_parse.ML Thu Mar 19 01:29:19 2009 -0700
11.2 +++ b/src/Pure/Isar/outer_parse.ML Thu Mar 19 11:51:49 2009 +0100
11.3 @@ -84,8 +84,8 @@
11.4 val fixes: (binding * string option * mixfix) list parser
11.5 val for_fixes: (binding * string option * mixfix) list parser
11.6 val for_simple_fixes: (binding * string option) list parser
11.7 - val ML_source: (SymbolPos.text * Position.T) parser
11.8 - val doc_source: (SymbolPos.text * Position.T) parser
11.9 + val ML_source: (Symbol_Pos.text * Position.T) parser
11.10 + val doc_source: (Symbol_Pos.text * Position.T) parser
11.11 val term_group: string parser
11.12 val prop_group: string parser
11.13 val term: string parser
12.1 --- a/src/Pure/Isar/outer_syntax.ML Thu Mar 19 01:29:19 2009 -0700
12.2 +++ b/src/Pure/Isar/outer_syntax.ML Thu Mar 19 11:51:49 2009 +0100
12.3 @@ -224,7 +224,7 @@
12.4 type isar =
12.5 (Toplevel.transition, (Toplevel.transition option,
12.6 (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
12.7 - (SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
12.8 + (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
12.9 Source.source) Source.source) Source.source) Source.source)
12.10 Source.source) Source.source) Source.source) Source.source;
12.11
13.1 --- a/src/Pure/Isar/proof_context.ML Thu Mar 19 01:29:19 2009 -0700
13.2 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 19 11:51:49 2009 +0100
13.3 @@ -430,7 +430,7 @@
13.4
13.5 local
13.6
13.7 -val token_content = Syntax.read_token #>> SymbolPos.content;
13.8 +val token_content = Syntax.read_token #>> Symbol_Pos.content;
13.9
13.10 fun prep_const_proper ctxt (c, pos) =
13.11 let val t as (Const (d, _)) =
14.1 --- a/src/Pure/ML/ml_context.ML Thu Mar 19 01:29:19 2009 -0700
14.2 +++ b/src/Pure/ML/ml_context.ML Thu Mar 19 11:51:49 2009 +0100
14.3 @@ -19,7 +19,7 @@
14.4 val the_global_context: unit -> theory
14.5 val the_local_context: unit -> Proof.context
14.6 val exec: (unit -> unit) -> Context.generic -> Context.generic
14.7 - val inherit_env: Proof.context -> Proof.context -> Proof.context
14.8 + val inherit_env: Context.generic -> Context.generic -> Context.generic
14.9 val name_space: ML_NameSpace.nameSpace
14.10 val stored_thms: thm list ref
14.11 val ml_store_thm: string * thm -> unit
14.12 @@ -29,10 +29,11 @@
14.13 (Proof.context -> string * string) * Proof.context
14.14 val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
14.15 val trace: bool ref
14.16 - val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
14.17 - val eval: bool -> Position.T -> string -> unit
14.18 + val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
14.19 + Position.T -> Symbol_Pos.text -> unit
14.20 + val eval: bool -> Position.T -> Symbol_Pos.text -> unit
14.21 val eval_file: Path.T -> unit
14.22 - val eval_in: Proof.context option -> bool -> Position.T -> string -> unit
14.23 + val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
14.24 val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
14.25 string * (unit -> 'a) option ref -> string -> 'a
14.26 val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
14.27 @@ -77,7 +78,7 @@
14.28 Symtab.merge (K true) (functor1, functor2));
14.29 );
14.30
14.31 -val inherit_env = Context.proof_map o ML_Env.put o ML_Env.get o Context.Proof;
14.32 +val inherit_env = ML_Env.put o ML_Env.get;
14.33
14.34 val name_space: ML_NameSpace.nameSpace =
14.35 let
14.36 @@ -191,12 +192,12 @@
14.37
14.38 fun eval_antiquotes (txt, pos) opt_context =
14.39 let
14.40 - val syms = SymbolPos.explode (txt, pos);
14.41 + val syms = Symbol_Pos.explode (txt, pos);
14.42 val ants = Antiquote.read (syms, pos);
14.43 val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
14.44 val ((ml_env, ml_body), opt_ctxt') =
14.45 if not (exists Antiquote.is_antiq ants)
14.46 - then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
14.47 + then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
14.48 else
14.49 let
14.50 val ctxt =
15.1 --- a/src/Pure/ML/ml_lex.ML Thu Mar 19 01:29:19 2009 -0700
15.2 +++ b/src/Pure/ML/ml_lex.ML Thu Mar 19 11:51:49 2009 +0100
15.3 @@ -18,7 +18,7 @@
15.4 val content_of: token -> string
15.5 val keywords: string list
15.6 val source: (Symbol.symbol, 'a) Source.source ->
15.7 - (token, (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source)
15.8 + (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
15.9 Source.source) Source.source
15.10 end;
15.11
15.12 @@ -75,9 +75,9 @@
15.13
15.14 (** scanners **)
15.15
15.16 -open BasicSymbolPos;
15.17 +open Basic_Symbol_Pos;
15.18
15.19 -fun !!! msg = SymbolPos.!!! ("SML lexical error: " ^ msg);
15.20 +fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
15.21
15.22
15.23 (* blanks *)
15.24 @@ -183,13 +183,13 @@
15.25
15.26 local
15.27
15.28 -fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss));
15.29 +fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss));
15.30
15.31 val scan = !!! "bad input"
15.32 (scan_char >> token Char ||
15.33 scan_string >> token String ||
15.34 scan_blanks1 >> token Space ||
15.35 - SymbolPos.scan_comment !!! >> token Comment ||
15.36 + Symbol_Pos.scan_comment !!! >> token Comment ||
15.37 Scan.max token_leq
15.38 (scan_keyword >> token Keyword)
15.39 (scan_word >> token Word ||
15.40 @@ -206,8 +206,8 @@
15.41 in
15.42
15.43 fun source src =
15.44 - SymbolPos.source (Position.line 1) src
15.45 - |> Source.source SymbolPos.stopper (Scan.bulk scan) (SOME (false, recover));
15.46 + Symbol_Pos.source (Position.line 1) src
15.47 + |> Source.source Symbol_Pos.stopper (Scan.bulk scan) (SOME (false, recover));
15.48
15.49 end;
15.50
16.1 --- a/src/Pure/Syntax/lexicon.ML Thu Mar 19 01:29:19 2009 -0700
16.2 +++ b/src/Pure/Syntax/lexicon.ML Thu Mar 19 11:51:49 2009 +0100
16.3 @@ -9,15 +9,15 @@
16.4 val is_identifier: string -> bool
16.5 val is_ascii_identifier: string -> bool
16.6 val is_tid: string -> bool
16.7 - val scan_id: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.8 - val scan_longid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.9 - val scan_tid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.10 - val scan_nat: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.11 - val scan_int: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.12 - val scan_hex: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.13 - val scan_bin: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.14 - val scan_var: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.15 - val scan_tvar: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
16.16 + val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.17 + val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.18 + val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.19 + val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.20 + val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.21 + val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.22 + val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.23 + val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.24 + val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
16.25 val implode_xstr: string list -> string
16.26 val explode_xstr: string -> string list
16.27 val read_indexname: string -> indexname
16.28 @@ -60,7 +60,7 @@
16.29 val matching_tokens: token * token -> bool
16.30 val valued_token: token -> bool
16.31 val predef_term: string -> token option
16.32 - val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list
16.33 + val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
16.34 end;
16.35
16.36 structure Lexicon: LEXICON =
16.37 @@ -88,9 +88,9 @@
16.38
16.39 (** basic scanners **)
16.40
16.41 -open BasicSymbolPos;
16.42 +open Basic_Symbol_Pos;
16.43
16.44 -fun !!! msg = SymbolPos.!!! ("Inner lexical error: " ^ msg);
16.45 +fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
16.46
16.47 val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
16.48 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
16.49 @@ -220,7 +220,7 @@
16.50 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
16.51
16.52 fun explode_xstr str =
16.53 - (case Scan.read SymbolPos.stopper scan_str_body (SymbolPos.explode (str, Position.none)) of
16.54 + (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
16.55 SOME cs => map symbol cs
16.56 | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
16.57
16.58 @@ -229,7 +229,7 @@
16.59 (** tokenize **)
16.60
16.61 fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
16.62 -fun token kind ss = Token (kind, SymbolPos.content ss, SymbolPos.range ss);
16.63 +fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
16.64
16.65 fun tokenize lex xids syms =
16.66 let
16.67 @@ -252,16 +252,16 @@
16.68 val scan_lit = Scan.literal lex >> token Literal;
16.69
16.70 val scan_token =
16.71 - SymbolPos.scan_comment !!! >> token Comment ||
16.72 + Symbol_Pos.scan_comment !!! >> token Comment ||
16.73 Scan.max token_leq scan_lit scan_val ||
16.74 scan_str >> token StrSy ||
16.75 Scan.many1 (Symbol.is_blank o symbol) >> token Space;
16.76 in
16.77 (case Scan.error
16.78 - (Scan.finite SymbolPos.stopper (Scan.repeat scan_token)) syms of
16.79 + (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
16.80 (toks, []) => toks
16.81 - | (_, ss) => error ("Inner lexical error at: " ^ SymbolPos.content ss ^
16.82 - Position.str_of (#1 (SymbolPos.range ss))))
16.83 + | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
16.84 + Position.str_of (#1 (Symbol_Pos.range ss))))
16.85 end;
16.86
16.87
16.88 @@ -303,7 +303,7 @@
16.89 (* indexname *)
16.90
16.91 fun read_indexname s =
16.92 - (case Scan.read SymbolPos.stopper scan_indexname (SymbolPos.explode (s, Position.none)) of
16.93 + (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
16.94 SOME xi => xi
16.95 | _ => error ("Lexical error in variable name: " ^ quote s));
16.96
16.97 @@ -317,16 +317,16 @@
16.98 fun read_var str =
16.99 let
16.100 val scan =
16.101 - $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one SymbolPos.is_eof) >> var ||
16.102 + $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
16.103 Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
16.104 - in the (Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none))) end;
16.105 + in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
16.106
16.107
16.108 (* read_variable *)
16.109
16.110 fun read_variable str =
16.111 let val scan = $$$ "?" |-- scan_indexname || scan_indexname
16.112 - in Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none)) end;
16.113 + in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
16.114
16.115
16.116 (* specific identifiers *)
16.117 @@ -341,14 +341,14 @@
16.118
16.119 fun nat cs =
16.120 Option.map (#1 o Library.read_int o map symbol)
16.121 - (Scan.read SymbolPos.stopper scan_nat cs);
16.122 + (Scan.read Symbol_Pos.stopper scan_nat cs);
16.123
16.124 in
16.125
16.126 -fun read_nat s = nat (SymbolPos.explode (s, Position.none));
16.127 +fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
16.128
16.129 fun read_int s =
16.130 - (case SymbolPos.explode (s, Position.none) of
16.131 + (case Symbol_Pos.explode (s, Position.none) of
16.132 ("-", _) :: cs => Option.map ~ (nat cs)
16.133 | cs => nat cs);
16.134
17.1 --- a/src/Pure/Syntax/simple_syntax.ML Thu Mar 19 01:29:19 2009 -0700
17.2 +++ b/src/Pure/Syntax/simple_syntax.ML Thu Mar 19 11:51:49 2009 +0100
17.3 @@ -21,7 +21,7 @@
17.4
17.5 fun read scan s =
17.6 (case
17.7 - SymbolPos.explode (s, Position.none) |>
17.8 + Symbol_Pos.explode (s, Position.none) |>
17.9 Lexicon.tokenize lexicon false |>
17.10 filter Lexicon.is_proper |>
17.11 Scan.read Lexicon.stopper scan of
18.1 --- a/src/Pure/Syntax/syntax.ML Thu Mar 19 01:29:19 2009 -0700
18.2 +++ b/src/Pure/Syntax/syntax.ML Thu Mar 19 11:51:49 2009 +0100
18.3 @@ -35,7 +35,7 @@
18.4 val print_trans: syntax -> unit
18.5 val print_syntax: syntax -> unit
18.6 val guess_infix: syntax -> string -> mixfix option
18.7 - val read_token: string -> SymbolPos.T list * Position.T
18.8 + val read_token: string -> Symbol_Pos.T list * Position.T
18.9 val ambiguity_is_error: bool ref
18.10 val ambiguity_level: int ref
18.11 val ambiguity_limit: int ref
18.12 @@ -43,12 +43,12 @@
18.13 (((string * int) * sort) list -> string * int -> Term.sort) ->
18.14 (string -> bool * string) -> (string -> string option) ->
18.15 (typ -> typ) -> (sort -> sort) -> Proof.context ->
18.16 - (string -> bool) -> syntax -> typ -> SymbolPos.T list * Position.T -> term
18.17 + (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
18.18 val standard_parse_typ: Proof.context -> syntax ->
18.19 ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
18.20 - SymbolPos.T list * Position.T -> typ
18.21 + Symbol_Pos.T list * Position.T -> typ
18.22 val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
18.23 - SymbolPos.T list * Position.T -> sort
18.24 + Symbol_Pos.T list * Position.T -> sort
18.25 datatype 'a trrule =
18.26 ParseRule of 'a * 'a |
18.27 PrintRule of 'a * 'a |
18.28 @@ -82,7 +82,7 @@
18.29 (string * string) trrule list -> syntax -> syntax
18.30 val update_trrules_i: ast trrule list -> syntax -> syntax
18.31 val remove_trrules_i: ast trrule list -> syntax -> syntax
18.32 - val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
18.33 + val parse_token: Markup.T -> string -> Symbol_Pos.T list * Position.T
18.34 val parse_sort: Proof.context -> string -> sort
18.35 val parse_typ: Proof.context -> string -> typ
18.36 val parse_term: Proof.context -> string -> term
18.37 @@ -467,7 +467,7 @@
18.38 | XML.Elem ("token", props, []) => ("", Position.of_properties props)
18.39 | XML.Text text => (text, Position.none)
18.40 | _ => (str, Position.none))
18.41 - in (SymbolPos.explode (text, pos), pos) end;
18.42 + in (Symbol_Pos.explode (text, pos), pos) end;
18.43
18.44
18.45 (* read_ast *)
19.1 --- a/src/Pure/Thy/latex.ML Thu Mar 19 01:29:19 2009 -0700
19.2 +++ b/src/Pure/Thy/latex.ML Thu Mar 19 11:51:49 2009 +0100
19.3 @@ -90,7 +90,7 @@
19.4 val output_syms_antiq =
19.5 (fn Antiquote.Text s => output_syms s
19.6 | Antiquote.Antiq (ss, _) =>
19.7 - enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map SymbolPos.symbol ss))
19.8 + enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
19.9 | Antiquote.Open _ => "{\\isaantiqopen}"
19.10 | Antiquote.Close _ => "{\\isaantiqclose}");
19.11
19.12 @@ -117,7 +117,7 @@
19.13 else if T.is_kind T.Verbatim tok then
19.14 let
19.15 val (txt, pos) = T.source_position_of tok;
19.16 - val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
19.17 + val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
19.18 val out = implode (map output_syms_antiq ants);
19.19 in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
19.20 else output_syms s
20.1 --- a/src/Pure/Thy/thy_output.ML Thu Mar 19 01:29:19 2009 -0700
20.2 +++ b/src/Pure/Thy/thy_output.ML Thu Mar 19 11:51:49 2009 +0100
20.3 @@ -22,7 +22,7 @@
20.4 ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
20.5 datatype markup = Markup | MarkupEnv | Verbatim
20.6 val modes: string list ref
20.7 - val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
20.8 + val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
20.9 val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
20.10 (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
20.11 val pretty_text: string -> Pretty.T
20.12 @@ -156,7 +156,7 @@
20.13 end
20.14 | expand (Antiquote.Open _) = ""
20.15 | expand (Antiquote.Close _) = "";
20.16 - val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
20.17 + val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
20.18 in
20.19 if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
20.20 error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
20.21 @@ -577,7 +577,7 @@
20.22 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
20.23 (fn {context, ...} => fn (txt, pos) =>
20.24 (ML_Context.eval_in (SOME context) false pos (ml txt);
20.25 - SymbolPos.content (SymbolPos.explode (txt, pos))
20.26 + Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
20.27 |> (if ! quotes then quote else I)
20.28 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
20.29 else
21.1 --- a/src/Pure/Thy/thy_syntax.ML Thu Mar 19 01:29:19 2009 -0700
21.2 +++ b/src/Pure/Thy/thy_syntax.ML Thu Mar 19 11:51:49 2009 +0100
21.3 @@ -7,7 +7,7 @@
21.4 signature THY_SYNTAX =
21.5 sig
21.6 val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
21.7 - (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
21.8 + (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
21.9 Source.source) Source.source) Source.source) Source.source
21.10 val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
21.11 val present_token: OuterLex.token -> output