# HG changeset patch
# User wenzelm
# Date 1237222009 -3600
# Node ID 0ed8fe16331a304926f6e5be11f811cbc4a4e270
# Parent  2ca69af4422ac25db13c26f7d99f2559879cbe51
adapted 'method_setup' command to Method.setup;

diff -r 2ca69af4422a -r 0ed8fe16331a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Mar 16 17:46:11 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 16 17:46:49 2009 +0100
@@ -334,7 +334,7 @@
 
 val _ =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
-    (P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
+    (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
     >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
 
 val _ =
diff -r 2ca69af4422a -r 0ed8fe16331a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 16 17:46:11 2009 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 16 17:46:49 2009 +0100
@@ -80,7 +80,7 @@
     -> 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 -> string * Position.T -> string -> theory -> theory
+  val method_setup: bstring * Position.T -> string * 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
@@ -404,9 +404,9 @@
 
 fun method_setup name (txt, pos) cmt =
   Context.theory_map (ML_Context.expression pos
-    "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
-    "Context.map_theory (Method.add_method method)"
-    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")"));
+    "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
+    "Context.map_theory (Method.setup name scan comment)"
+    ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));