# HG changeset patch
# User wenzelm
# Date 1408548227 -7200
# Node ID 5bdb58845eabf9087880038f1261825c93882ca9
# Parent  28e5ccf4a27f34befe05b0ddacd4a43ce0d895d7
support for declaration within token source;

diff -r 28e5ccf4a27f -r 5bdb58845eab src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Aug 20 16:06:10 2014 +0200
+++ b/src/Pure/Isar/args.ML	Wed Aug 20 17:23:47 2014 +0200
@@ -39,12 +39,14 @@
   val internal_term: term parser
   val internal_fact: thm list parser
   val internal_attribute: (morphism -> attribute) parser
+  val internal_declaration: declaration parser
   val named_source: (Token.T -> Token.src) -> Token.src parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> string option * thm list) -> thm list parser
-  val named_attribute:
-    (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
+  val named_attribute: (string * Position.T -> morphism -> attribute) ->
+    (morphism -> attribute) parser
+  val text_declaration: (Symbol_Pos.source -> declaration) -> declaration parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
@@ -137,6 +139,7 @@
 val internal_term = value (fn Token.Term t => t);
 val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
+val internal_declaration = value (fn Token.Declaration decl => decl);
 
 fun named_source read = internal_source || named >> evaluate Token.Source read;
 
@@ -152,6 +155,10 @@
   internal_attribute ||
   named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
 
+fun text_declaration read =
+  internal_declaration ||
+  text_token >> evaluate Token.Declaration (read o Token.source_position_of);
+
 
 (* terms and types *)
 
diff -r 28e5ccf4a27f -r 5bdb58845eab src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Aug 20 16:06:10 2014 +0200
+++ b/src/Pure/Isar/token.ML	Wed Aug 20 17:23:47 2014 +0200
@@ -22,6 +22,7 @@
     Term of term |
     Fact of string option * thm list |
     Attribute of morphism -> attribute |
+    Declaration of declaration |
     Files of file Exn.result list
   val name0: string -> value
   val pos_of: T -> Position.T
@@ -163,6 +164,7 @@
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
+  Declaration of declaration |
   Files of file Exn.result list;
 
 fun name0 a = Name (a, Morphism.identity);
@@ -421,6 +423,7 @@
     | Term t => Term (Morphism.term phi t)
     | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
     | Attribute att => Attribute (Morphism.transform phi att)
+    | Declaration decl => Declaration (Morphism.transform phi decl)
     | Files _ => v))
 and transform_src phi = map_args (transform phi);