Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more precise type Symbol_Pos.text;
authorwenzelm
Wed, 18 Mar 2009 22:41:14 +0100
changeset 30575 368e26dfba69
parent 30574 b9bcc640ed58
child 30576 7e5b9bbc54d8
more precise type Symbol_Pos.text;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 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	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 22:41:14 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 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
--- a/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 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
isabelle