--- a/NEWS Thu Mar 19 01:29:19 2009 -0700
+++ b/NEWS Thu Mar 19 11:51:49 2009 +0100
@@ -176,30 +176,28 @@
* The 'axiomatization' command now only works within a global theory
context. INCOMPATIBILITY.
-* New find_theorems criterion "solves" matching theorems that directly
-solve the current goal. Try "find_theorems solves".
-
-* Added an auto solve option, which can be enabled through the
-ProofGeneral Isabelle settings menu (disabled by default).
-
-When enabled, find_theorems solves is called whenever a new lemma is
-stated. Any theorems that could solve the lemma directly are listed
-underneath the goal.
-
-* New command 'find_consts' searches for constants based on type and
-name patterns, e.g.
+* New 'find_theorems' criterion "solves" matching theorems that
+directly solve the current goal.
+
+* Auto solve feature for main theorem statements (cf. option in Proof
+General Isabelle settings menu, enabled by default). Whenever a new
+goal is stated, "find_theorems solves" is called; any theorems that
+could solve the lemma directly are listed underneath the goal.
+
+* Command 'find_consts' searches for constants based on type and name
+patterns, e.g.
find_consts "_ => bool"
By default, matching is against subtypes, but it may be restricted to
-the whole type. Searching by name is possible. Multiple queries are
+the whole type. Searching by name is possible. Multiple queries are
conjunctive and queries may be negated by prefixing them with a
hyphen:
find_consts strict: "_ => bool" name: "Int" -"int => int"
-* New command 'local_setup' is similar to 'setup', but operates on a
-local theory context.
+* Command 'local_setup' is similar to 'setup', but operates on a local
+theory context.
*** Document preparation ***
--- a/src/Pure/General/symbol_pos.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/General/symbol_pos.ML Thu Mar 19 11:51:49 2009 +0100
@@ -34,7 +34,7 @@
val explode: text * Position.T -> T list
end;
-structure SymbolPos: SYMBOL_POS =
+structure Symbol_Pos: SYMBOL_POS =
struct
(* type T *)
@@ -149,5 +149,5 @@
end;
-structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos; (*not open by default*)
+structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos; (*not open by default*)
--- a/src/Pure/Isar/antiquote.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/antiquote.ML Thu Mar 19 11:51:49 2009 +0100
@@ -7,12 +7,12 @@
signature ANTIQUOTE =
sig
datatype antiquote =
- Text of string | Antiq of SymbolPos.T list * Position.T |
+ Text of string | Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T | Close of Position.T
val is_antiq: antiquote -> bool
- val read: SymbolPos.T list * Position.T -> antiquote list
+ val read: Symbol_Pos.T list * Position.T -> antiquote list
val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
- SymbolPos.T list * Position.T -> 'a
+ Symbol_Pos.T list * Position.T -> 'a
end;
structure Antiquote: ANTIQUOTE =
@@ -22,7 +22,7 @@
datatype antiquote =
Text of string |
- Antiq of SymbolPos.T list * Position.T |
+ Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T |
Close of Position.T;
@@ -48,7 +48,7 @@
(* scan_antiquote *)
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
structure T = OuterLex;
local
@@ -63,18 +63,18 @@
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
val scan_antiq =
- SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+ Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
T.!!! "missing closing brace of antiquotation"
- (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
+ (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
>> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
in
val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
+ (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
scan_antiq ||
- SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
- SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
+ Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
+ Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
end;
@@ -86,7 +86,7 @@
fun read ([], _) = []
| read (syms, pos) =
- (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
@@ -96,7 +96,7 @@
fun read_antiq lex scan (syms, pos) =
let
fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ SymbolPos.content syms ^ "}");
+ "@{" ^ Symbol_Pos.content syms ^ "}");
val res =
Source.of_list syms
--- a/src/Pure/Isar/args.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/args.ML Thu Mar 19 11:51:49 2009 +0100
@@ -32,7 +32,7 @@
val mode: string -> bool context_parser
val maybe: 'a parser -> 'a option parser
val name_source: string parser
- val name_source_position: (SymbolPos.text * Position.T) parser
+ val name_source_position: (Symbol_Pos.text * Position.T) parser
val name: string parser
val binding: binding parser
val alt_name: string parser
--- a/src/Pure/Isar/attrib.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/attrib.ML Thu Mar 19 11:51:49 2009 +0100
@@ -26,7 +26,8 @@
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
val syntax: attribute context_parser -> src -> attribute
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
- val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+ val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+ theory -> theory
val no_args: attribute -> src -> attribute
val add_del: attribute -> attribute -> attribute context_parser
val add_del_args: attribute -> attribute -> src -> attribute
--- a/src/Pure/Isar/isar_cmd.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 19 11:51:49 2009 +0100
@@ -6,18 +6,18 @@
signature ISAR_CMD =
sig
- val global_setup: string * Position.T -> theory -> theory
- val local_setup: string * Position.T -> Proof.context -> Proof.context
- val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
- val parse_translation: bool * (string * Position.T) -> theory -> theory
- val print_translation: bool * (string * Position.T) -> theory -> theory
- val typed_print_translation: bool * (string * Position.T) -> theory -> theory
- val print_ast_translation: bool * (string * Position.T) -> theory -> theory
- val oracle: bstring * Position.T -> SymbolPos.text * Position.T -> theory -> theory
+ val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
+ val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
+ val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
- val declaration: string * Position.T -> local_theory -> local_theory
- val simproc_setup: string -> string list -> string * Position.T -> string list ->
+ val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
+ val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
local_theory -> local_theory
val hide_names: bool -> string * xstring list -> theory -> theory
val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -38,7 +38,7 @@
val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
val disable_pr: Toplevel.transition -> Toplevel.transition
val enable_pr: Toplevel.transition -> Toplevel.transition
- val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
+ val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
val cd: Path.T -> Toplevel.transition -> Toplevel.transition
val pwd: Toplevel.transition -> Toplevel.transition
val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
@@ -75,10 +75,10 @@
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
- val header_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
- val local_theory_markup: xstring option * (SymbolPos.text * Position.T) ->
+ val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+ val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
Toplevel.transition -> Toplevel.transition
- val proof_markup: SymbolPos.text * Position.T -> Toplevel.transition -> Toplevel.transition
+ val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
end;
structure IsarCmd: ISAR_CMD =
@@ -152,7 +152,7 @@
fun oracle (name, pos) (body_txt, body_pos) =
let
- val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
+ val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));
val txt =
"local\n\
\ val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 19 11:51:49 2009 +0100
@@ -272,7 +272,7 @@
OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
val _ =
- OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
+ OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
(P.and_list1 SpecParse.xthms1
>> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
@@ -295,28 +295,35 @@
(* use ML text *)
+fun inherit_env (context as Context.Proof lthy) =
+ Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+ | inherit_env context = context;
+
+fun inherit_env_prf prf = Proof.map_contexts
+ (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+
val _ =
- OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.thy_decl)
- (P.path >> (Toplevel.generic_theory o ThyInfo.exec_file false));
+ OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
+ (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
val _ =
- OuterSyntax.command "ML" "eval ML text within theory" (K.tag_ml K.thy_decl)
+ OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
(P.ML_source >> (fn (txt, pos) =>
- Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
+ Toplevel.generic_theory
+ (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
val _ =
- OuterSyntax.command "ML_prf" "eval ML text within proof" (K.tag_proof K.prf_decl)
+ OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
(P.ML_source >> (fn (txt, pos) =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #>
- (fn prf => Proof.map_contexts (ML_Context.inherit_env (Proof.context_of prf)) prf))));
+ (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
val _ =
- OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
+ OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
(P.ML_source >> IsarCmd.ml_diag true);
val _ =
- OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
+ OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
(P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
val _ =
--- a/src/Pure/Isar/local_theory.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/local_theory.ML Thu Mar 19 11:51:49 2009 +0100
@@ -23,6 +23,7 @@
val theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
+ val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
val affirm: local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
@@ -163,6 +164,11 @@
fun target f = #2 o target_result (f #> pair ());
+fun map_contexts f =
+ theory (Context.theory_map f) #>
+ target (Context.proof_map f) #>
+ Context.proof_map f;
+
(* basic operations *)
--- a/src/Pure/Isar/method.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/method.ML Thu Mar 19 11:51:49 2009 +0100
@@ -81,7 +81,8 @@
-> theory -> theory
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
- val method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+ val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+ theory -> theory
val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
val no_args: method -> src -> Proof.context -> method
--- a/src/Pure/Isar/outer_lex.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_lex.ML Thu Mar 19 11:51:49 2009 +0100
@@ -35,7 +35,7 @@
val is_blank: token -> bool
val is_newline: token -> bool
val source_of: token -> string
- val source_position_of: token -> SymbolPos.text * Position.T
+ val source_position_of: token -> Symbol_Pos.text * Position.T
val content_of: token -> string
val unparse: token -> string
val text_of: token -> string * string
@@ -50,14 +50,14 @@
val assign: value option -> token -> unit
val closure: token -> token
val ident_or_symbolic: string -> bool
- val !!! : string -> (SymbolPos.T list -> 'a) -> SymbolPos.T list -> 'a
- val scan_quoted: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
+ val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
+ val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- (SymbolPos.T, 'a) Source.source -> (token, (SymbolPos.T, 'a) Source.source) Source.source
+ (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
- (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
end;
structure OuterLex: OUTER_LEX =
@@ -92,7 +92,7 @@
Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
Malformed | Error of string | Sync | EOF;
-datatype token = Token of (SymbolPos.text * Position.range) * (token_kind * string) * slot;
+datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
val str_of_kind =
fn Command => "command"
@@ -259,9 +259,9 @@
(** scanners **)
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
-fun !!! msg = SymbolPos.!!! ("Outer lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
fun change_prompt scan = Scan.prompt "# " scan;
@@ -303,8 +303,8 @@
Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
fun scan_strs q =
- (SymbolPos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
- (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- SymbolPos.scan_pos)));
+ (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
+ (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos)));
in
@@ -323,8 +323,8 @@
Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
val scan_verbatim =
- (SymbolPos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
- (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- SymbolPos.scan_pos)));
+ (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
+ (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
(* scan space *)
@@ -339,7 +339,7 @@
(* scan comment *)
val scan_comment =
- SymbolPos.scan_pos -- (SymbolPos.scan_comment_body !!! -- SymbolPos.scan_pos);
+ Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
(* scan malformed symbols *)
@@ -360,10 +360,10 @@
fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
fun token k ss =
- Token ((SymbolPos.implode ss, SymbolPos.range ss), (k, SymbolPos.untabify_content ss), Slot);
+ Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
fun token_range k (pos1, (ss, pos2)) =
- Token (SymbolPos.implode_range pos1 pos2 ss, (k, SymbolPos.untabify_content ss), Slot);
+ Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
fun scan (lex1, lex2) = !!! "bad input"
(scan_string >> token_range String ||
@@ -392,11 +392,11 @@
in
fun source' {do_recover} get_lex =
- Source.source SymbolPos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
+ Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
(Option.map (rpair recover) do_recover);
fun source do_recover get_lex pos src =
- SymbolPos.source pos src
+ Symbol_Pos.source pos src
|> source' do_recover get_lex;
end;
--- a/src/Pure/Isar/outer_parse.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_parse.ML Thu Mar 19 11:51:49 2009 +0100
@@ -84,8 +84,8 @@
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
val for_simple_fixes: (binding * string option) list parser
- val ML_source: (SymbolPos.text * Position.T) parser
- val doc_source: (SymbolPos.text * Position.T) parser
+ val ML_source: (Symbol_Pos.text * Position.T) parser
+ val doc_source: (Symbol_Pos.text * Position.T) parser
val term_group: string parser
val prop_group: string parser
val term: string parser
--- a/src/Pure/Isar/outer_syntax.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Thu Mar 19 11:51:49 2009 +0100
@@ -224,7 +224,7 @@
type isar =
(Toplevel.transition, (Toplevel.transition option,
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
- (SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
+ (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
Source.source) Source.source) Source.source) Source.source)
Source.source) Source.source) Source.source) Source.source;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 19 11:51:49 2009 +0100
@@ -430,7 +430,7 @@
local
-val token_content = Syntax.read_token #>> SymbolPos.content;
+val token_content = Syntax.read_token #>> Symbol_Pos.content;
fun prep_const_proper ctxt (c, pos) =
let val t as (Const (d, _)) =
--- a/src/Pure/ML/ml_context.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/ML/ml_context.ML Thu Mar 19 11:51:49 2009 +0100
@@ -19,7 +19,7 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val inherit_env: Proof.context -> Proof.context -> Proof.context
+ val inherit_env: Context.generic -> Context.generic -> Context.generic
val name_space: ML_NameSpace.nameSpace
val stored_thms: thm list ref
val ml_store_thm: string * thm -> unit
@@ -29,10 +29,11 @@
(Proof.context -> string * string) * Proof.context
val add_antiq: string -> (Position.T -> antiq context_parser) -> unit
val trace: bool ref
- val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
- val eval: bool -> Position.T -> string -> unit
+ val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
+ Position.T -> Symbol_Pos.text -> unit
+ val eval: bool -> Position.T -> Symbol_Pos.text -> unit
val eval_file: Path.T -> unit
- val eval_in: Proof.context option -> bool -> Position.T -> string -> unit
+ val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
string * (unit -> 'a) option ref -> string -> 'a
val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
@@ -77,7 +78,7 @@
Symtab.merge (K true) (functor1, functor2));
);
-val inherit_env = Context.proof_map o ML_Env.put o ML_Env.get o Context.Proof;
+val inherit_env = ML_Env.put o ML_Env.get;
val name_space: ML_NameSpace.nameSpace =
let
@@ -191,12 +192,12 @@
fun eval_antiquotes (txt, pos) opt_context =
let
- val syms = SymbolPos.explode (txt, pos);
+ val syms = Symbol_Pos.explode (txt, pos);
val ants = Antiquote.read (syms, pos);
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
if not (exists Antiquote.is_antiq ants)
- then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
+ then (("", Symbol.escape (Symbol_Pos.content syms)), opt_ctxt)
else
let
val ctxt =
--- a/src/Pure/ML/ml_lex.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML Thu Mar 19 11:51:49 2009 +0100
@@ -18,7 +18,7 @@
val content_of: token -> string
val keywords: string list
val source: (Symbol.symbol, 'a) Source.source ->
- (token, (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source)
+ (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
Source.source) Source.source
end;
@@ -75,9 +75,9 @@
(** scanners **)
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
-fun !!! msg = SymbolPos.!!! ("SML lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
(* blanks *)
@@ -183,13 +183,13 @@
local
-fun token k ss = Token (SymbolPos.range ss, (k, SymbolPos.implode ss));
+fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss));
val scan = !!! "bad input"
(scan_char >> token Char ||
scan_string >> token String ||
scan_blanks1 >> token Space ||
- SymbolPos.scan_comment !!! >> token Comment ||
+ Symbol_Pos.scan_comment !!! >> token Comment ||
Scan.max token_leq
(scan_keyword >> token Keyword)
(scan_word >> token Word ||
@@ -206,8 +206,8 @@
in
fun source src =
- SymbolPos.source (Position.line 1) src
- |> Source.source SymbolPos.stopper (Scan.bulk scan) (SOME (false, recover));
+ Symbol_Pos.source (Position.line 1) src
+ |> Source.source Symbol_Pos.stopper (Scan.bulk scan) (SOME (false, recover));
end;
--- a/src/Pure/Syntax/lexicon.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/lexicon.ML Thu Mar 19 11:51:49 2009 +0100
@@ -9,15 +9,15 @@
val is_identifier: string -> bool
val is_ascii_identifier: string -> bool
val is_tid: string -> bool
- val scan_id: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_longid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_tid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_nat: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_int: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_hex: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_bin: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_var: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
- val scan_tvar: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
+ val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
+ val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val implode_xstr: string list -> string
val explode_xstr: string -> string list
val read_indexname: string -> indexname
@@ -60,7 +60,7 @@
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
- val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list
+ val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
end;
structure Lexicon: LEXICON =
@@ -88,9 +88,9 @@
(** basic scanners **)
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
-fun !!! msg = SymbolPos.!!! ("Inner lexical error: " ^ msg);
+fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
@@ -220,7 +220,7 @@
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
fun explode_xstr str =
- (case Scan.read SymbolPos.stopper scan_str_body (SymbolPos.explode (str, Position.none)) of
+ (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
SOME cs => map symbol cs
| _ => error ("Inner lexical error: literal string expected at " ^ quote str));
@@ -229,7 +229,7 @@
(** tokenize **)
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
-fun token kind ss = Token (kind, SymbolPos.content ss, SymbolPos.range ss);
+fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
fun tokenize lex xids syms =
let
@@ -252,16 +252,16 @@
val scan_lit = Scan.literal lex >> token Literal;
val scan_token =
- SymbolPos.scan_comment !!! >> token Comment ||
+ Symbol_Pos.scan_comment !!! >> token Comment ||
Scan.max token_leq scan_lit scan_val ||
scan_str >> token StrSy ||
Scan.many1 (Symbol.is_blank o symbol) >> token Space;
in
(case Scan.error
- (Scan.finite SymbolPos.stopper (Scan.repeat scan_token)) syms of
+ (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
(toks, []) => toks
- | (_, ss) => error ("Inner lexical error at: " ^ SymbolPos.content ss ^
- Position.str_of (#1 (SymbolPos.range ss))))
+ | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
+ Position.str_of (#1 (Symbol_Pos.range ss))))
end;
@@ -303,7 +303,7 @@
(* indexname *)
fun read_indexname s =
- (case Scan.read SymbolPos.stopper scan_indexname (SymbolPos.explode (s, Position.none)) of
+ (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
SOME xi => xi
| _ => error ("Lexical error in variable name: " ^ quote s));
@@ -317,16 +317,16 @@
fun read_var str =
let
val scan =
- $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one SymbolPos.is_eof) >> var ||
+ $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
- in the (Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none))) end;
+ in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
(* read_variable *)
fun read_variable str =
let val scan = $$$ "?" |-- scan_indexname || scan_indexname
- in Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none)) end;
+ in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
(* specific identifiers *)
@@ -341,14 +341,14 @@
fun nat cs =
Option.map (#1 o Library.read_int o map symbol)
- (Scan.read SymbolPos.stopper scan_nat cs);
+ (Scan.read Symbol_Pos.stopper scan_nat cs);
in
-fun read_nat s = nat (SymbolPos.explode (s, Position.none));
+fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
fun read_int s =
- (case SymbolPos.explode (s, Position.none) of
+ (case Symbol_Pos.explode (s, Position.none) of
("-", _) :: cs => Option.map ~ (nat cs)
| cs => nat cs);
--- a/src/Pure/Syntax/simple_syntax.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/simple_syntax.ML Thu Mar 19 11:51:49 2009 +0100
@@ -21,7 +21,7 @@
fun read scan s =
(case
- SymbolPos.explode (s, Position.none) |>
+ Symbol_Pos.explode (s, Position.none) |>
Lexicon.tokenize lexicon false |>
filter Lexicon.is_proper |>
Scan.read Lexicon.stopper scan of
--- a/src/Pure/Syntax/syntax.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Syntax/syntax.ML Thu Mar 19 11:51:49 2009 +0100
@@ -35,7 +35,7 @@
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
val guess_infix: syntax -> string -> mixfix option
- val read_token: string -> SymbolPos.T list * Position.T
+ val read_token: string -> Symbol_Pos.T list * Position.T
val ambiguity_is_error: bool ref
val ambiguity_level: int ref
val ambiguity_limit: int ref
@@ -43,12 +43,12 @@
(((string * int) * sort) list -> string * int -> Term.sort) ->
(string -> bool * string) -> (string -> string option) ->
(typ -> typ) -> (sort -> sort) -> Proof.context ->
- (string -> bool) -> syntax -> typ -> SymbolPos.T list * Position.T -> term
+ (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
- SymbolPos.T list * Position.T -> typ
+ Symbol_Pos.T list * Position.T -> typ
val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
- SymbolPos.T list * Position.T -> sort
+ Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
ParseRule of 'a * 'a |
PrintRule of 'a * 'a |
@@ -82,7 +82,7 @@
(string * string) trrule list -> syntax -> syntax
val update_trrules_i: ast trrule list -> syntax -> syntax
val remove_trrules_i: ast trrule list -> syntax -> syntax
- val parse_token: Markup.T -> string -> SymbolPos.T list * Position.T
+ val parse_token: Markup.T -> string -> Symbol_Pos.T list * Position.T
val parse_sort: Proof.context -> string -> sort
val parse_typ: Proof.context -> string -> typ
val parse_term: Proof.context -> string -> term
@@ -467,7 +467,7 @@
| XML.Elem ("token", props, []) => ("", Position.of_properties props)
| XML.Text text => (text, Position.none)
| _ => (str, Position.none))
- in (SymbolPos.explode (text, pos), pos) end;
+ in (Symbol_Pos.explode (text, pos), pos) end;
(* read_ast *)
--- a/src/Pure/Thy/latex.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/latex.ML Thu Mar 19 11:51:49 2009 +0100
@@ -90,7 +90,7 @@
val output_syms_antiq =
(fn Antiquote.Text s => output_syms s
| Antiquote.Antiq (ss, _) =>
- enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map SymbolPos.symbol ss))
+ enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
| Antiquote.Open _ => "{\\isaantiqopen}"
| Antiquote.Close _ => "{\\isaantiqclose}");
@@ -117,7 +117,7 @@
else if T.is_kind T.Verbatim tok then
let
val (txt, pos) = T.source_position_of tok;
- val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else output_syms s
--- a/src/Pure/Thy/thy_output.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 19 11:51:49 2009 +0100
@@ -22,7 +22,7 @@
({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
- val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
+ val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
val pretty_text: string -> Pretty.T
@@ -156,7 +156,7 @@
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
@@ -577,7 +577,7 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
(fn {context, ...} => fn (txt, pos) =>
(ML_Context.eval_in (SOME context) false pos (ml txt);
- SymbolPos.content (SymbolPos.explode (txt, pos))
+ Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else
--- a/src/Pure/Thy/thy_syntax.ML Thu Mar 19 01:29:19 2009 -0700
+++ b/src/Pure/Thy/thy_syntax.ML Thu Mar 19 11:51:49 2009 +0100
@@ -7,7 +7,7 @@
signature THY_SYNTAX =
sig
val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
- (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
+ (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
Source.source) Source.source) Source.source) Source.source
val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
val present_token: OuterLex.token -> output