# HG changeset patch
# User wenzelm
# Date 1428000404 -7200
# Node ID 7d5b2f4c621c6f2ce4d22fb2589753e6187c3334
# Parent  0655a7217e1479657228006e709ab141daa91c5d# Parent  d1ddcd8df4e4589e00a0ee212236432bce3506ee
merged

diff -r 0655a7217e14 -r 7d5b2f4c621c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Apr 02 11:22:24 2015 +0200
+++ b/src/Pure/General/name_space.ML	Thu Apr 02 20:46:44 2015 +0200
@@ -32,6 +32,7 @@
   val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
   val merge: T * T -> T
   type naming
+  val get_scopes: naming -> Binding.scope list
   val get_scope: naming -> Binding.scope option
   val new_scope: naming -> Binding.scope * naming
   val private: Binding.scope -> naming -> naming
diff -r 0655a7217e14 -r 7d5b2f4c621c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Apr 02 11:22:24 2015 +0200
+++ b/src/Pure/Isar/method.ML	Thu Apr 02 20:46:44 2015 +0200
@@ -372,6 +372,10 @@
 fun check_src ctxt =
   #1 o Token.check_src ctxt (get_methods (Context.Proof ctxt));
 
+fun checked_info ctxt name =
+  let val space = Name_Space.space_of_table (get_methods (Context.Proof ctxt))
+  in (Name_Space.kind_of space, Name_Space.markup space name) end;
+
 
 (* method setup *)
 
@@ -574,7 +578,7 @@
         NONE => (Parse.xname, Token.src)
       | SOME ctxt =>
          (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
-          fn name => fn args => check_src ctxt (Token.src name args)));
+          fn (name, pos) => fn args => Token.src_checked (name, pos) args (checked_info ctxt name)));
 
     fun meth5 x =
      (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||
@@ -586,8 +590,8 @@
         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
       meth5 -- Parse.position (Parse.$$$ "+")
         >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
-      meth5 --
-        (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
+      meth5 -- (Parse.position (Parse.$$$ "[") --
+          Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
         >> (fn (m, (((_, pos1), n), (_, pos2))) =>
             Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
       meth5) x
diff -r 0655a7217e14 -r 7d5b2f4c621c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Apr 02 11:22:24 2015 +0200
+++ b/src/Pure/Isar/token.ML	Thu Apr 02 20:46:44 2015 +0200
@@ -32,6 +32,7 @@
   val pos_of: T -> Position.T
   val range_of: T list -> Position.range
   val src: xstring * Position.T -> T list -> src
+  val src_checked: string * Position.T -> T list -> string * Markup.T -> src
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> T list
   val range_of_src: src -> Position.T
@@ -161,7 +162,7 @@
   Src of
    {name: string * Position.T,
     args: T list,
-    checked_markup: (string * Markup.T) option}
+    checked: (string * Markup.T) option}
 
 and slot =
   Slot |
@@ -195,10 +196,11 @@
 
 (* src *)
 
-fun src name args = Src {name = name, args = args, checked_markup = NONE};
+fun src name args = Src {name = name, args = args, checked = NONE};
+fun src_checked name args checked = Src {name = name, args = args, checked = SOME checked};
 
-fun map_args f (Src {name, args, checked_markup}) =
-  Src {name = name, args = map f args, checked_markup = checked_markup};
+fun map_args f (Src {name, args, checked}) =
+  Src {name = name, args = map f args, checked = checked};
 
 fun name_of_src (Src {name, ...}) = name;
 fun args_of_src (Src {args, ...}) = args;
@@ -207,15 +209,15 @@
   if null args then pos
   else Position.set_range (pos, #2 (range_of args));
 
-fun check_src _ table (src as Src {name = (name, _), checked_markup = SOME _, ...}) =
+fun check_src _ table (src as Src {name = (name, _), checked = SOME _, ...}) =
       (src, Name_Space.get table name)
-  | check_src ctxt table (Src {name = (xname, pos), args, checked_markup = NONE}) =
+  | check_src ctxt table (Src {name = (xname, pos), args, checked = NONE}) =
       let
         val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
         val space = Name_Space.space_of_table table;
         val kind = Name_Space.kind_of space;
         val markup = Name_Space.markup space name;
-      in (Src {name = (name, pos), args = args, checked_markup = SOME (kind, markup)}, x) end;
+      in (src_checked (name, pos) args (kind, markup), x) end;
 
 
 (* stopper *)
@@ -478,9 +480,9 @@
 
 fun pretty_src ctxt src =
   let
-    val Src {name = (name, _), args, checked_markup} = src;
+    val Src {name = (name, _), args, checked} = src;
     val prt_name =
-      (case checked_markup of
+      (case checked of
         NONE => Pretty.str name
       | SOME (_, markup) => Pretty.mark_str (markup, name));
     val prt_arg = pretty_value ctxt;
@@ -663,7 +665,7 @@
 
 (* wrapped syntax *)
 
-fun syntax_generic scan (Src {name = (name, pos), args = args0, checked_markup}) context =
+fun syntax_generic scan (Src {name = (name, pos), args = args0, checked}) context =
   let
     val args1 = map init_assignable args0;
     fun reported_text () =
@@ -679,7 +681,7 @@
     | (_, (_, args2)) =>
         let
           val print_name =
-            (case checked_markup of
+            (case checked of
               NONE => quote name
             | SOME (kind, markup) => plain_words kind ^ " " ^ quote (Markup.markup markup name));
           val print_args =
@@ -696,4 +698,3 @@
 
 type 'a parser = 'a Token.parser;
 type 'a context_parser = 'a Token.context_parser;
-