# HG changeset patch
# User wenzelm
# Date 1303067865 -7200
# Node ID 9371ea9f91fb58408925a38b861fe7a07a71495c
# Parent  26f64dddf2c6fbd01fd45bbe591a2ebd8c0f54c6
markup attributes/methods via name space;
eliminated obsolete markup;

diff -r 26f64dddf2c6 -r 9371ea9f91fb src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Apr 17 21:04:22 2011 +0200
+++ b/src/Pure/General/markup.ML	Sun Apr 17 21:17:45 2011 +0200
@@ -55,8 +55,6 @@
   val typN: string val typ: T
   val termN: string val term: T
   val propN: string val prop: T
-  val attributeN: string val attribute: string -> T
-  val methodN: string val method: string -> T
   val ML_keywordN: string val ML_keyword: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_identN: string val ML_ident: T
@@ -237,9 +235,6 @@
 val (termN, term) = markup_elem "term";
 val (propN, prop) = markup_elem "prop";
 
-val (attributeN, attribute) = markup_string "attribute" nameN;
-val (methodN, method) = markup_string "method" nameN;
-
 
 (* ML syntax *)
 
diff -r 26f64dddf2c6 -r 9371ea9f91fb src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 17 21:04:22 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 17 21:17:45 2011 +0200
@@ -109,12 +109,12 @@
 
 fun attribute_i thy =
   let
-    val attrs = #2 (Attributes.get thy);
+    val (space, tab) = Attributes.get thy;
     fun attr src =
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup attrs name of
+        (case Symtab.lookup tab name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME (att, _) => (Position.report pos (Markup.attribute name); att src))
+        | SOME (att, _) => (Position.report pos (Name_Space.markup space name); att src))
       end;
   in attr end;
 
diff -r 26f64dddf2c6 -r 9371ea9f91fb src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Apr 17 21:04:22 2011 +0200
+++ b/src/Pure/Isar/method.ML	Sun Apr 17 21:17:45 2011 +0200
@@ -356,12 +356,12 @@
 
 fun method_i thy =
   let
-    val meths = #2 (Methods.get thy);
+    val (space, tab) = Methods.get thy;
     fun meth src =
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup meths name of
+        (case Symtab.lookup tab name of
           NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
-        | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
+        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
       end;
   in meth end;
 
diff -r 26f64dddf2c6 -r 9371ea9f91fb src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 21:04:22 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 21:17:45 2011 +0200
@@ -173,8 +173,6 @@
       Markup.TYP -> NULL,
       Markup.TERM -> NULL,
       Markup.PROP -> NULL,
-      Markup.ATTRIBUTE -> NULL,
-      Markup.METHOD -> NULL,
       // ML syntax
       Markup.ML_KEYWORD -> KEYWORD1,
       Markup.ML_DELIMITER -> OPERATOR,