# HG changeset patch
# User wenzelm
# Date 1321285939 -3600
# Node ID 6d71d9e523699505f2f1464501b6396f3ee197e8
# Parent  ae60518ac054d7cb45d8f837b5b82f20b1e525fd
pass positions for named targets, for formal links in the document model;

diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -77,7 +77,7 @@
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
-  val local_theory_markup: xstring option * (Symbol_Pos.text * Position.T) ->
+  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
     Toplevel.transition -> Toplevel.transition
   val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
 end;
diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -394,7 +394,7 @@
 
 val _ =
   Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
-    (Parse.name --| Parse.begin >> (fn name =>
+    (Parse.position Parse.name --| Parse.begin >> (fn name =>
       Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
 
 
diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -37,6 +37,7 @@
     (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
     (string * morphism) list -> theory -> theory
   val intern: theory -> xstring -> string
+  val check: theory -> xstring * Position.T -> string
   val extern: theory -> string -> xstring
   val defined: theory -> string -> bool
   val params_of: theory -> string -> ((string * typ) * mixfix) list
@@ -162,6 +163,7 @@
 );
 
 val intern = Name_Space.intern o #1 o Locales.get;
+fun check thy = #1 o Name_Space.check (Proof_Context.init_global thy) (Locales.get thy);
 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -10,7 +10,7 @@
   val init: (local_theory -> local_theory) -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val reinit: local_theory -> local_theory -> local_theory
-  val context_cmd: xstring -> theory -> local_theory
+  val context_cmd: xstring * Position.T -> theory -> local_theory
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
 end;
 
@@ -209,7 +209,7 @@
       init before_exit target o Local_Theory.exit_global
   | NONE => error "Not in a named target");
 
-fun context_cmd "-" thy = init I "" thy
-  | context_cmd target thy = init I (Locale.intern thy target) thy;
+fun context_cmd ("-", _) thy = init I "" thy
+  | context_cmd target thy = init I (Locale.check thy target) thy;
 
 end;
diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/parse.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -99,8 +99,8 @@
   val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
-  val target: xstring parser
-  val opt_target: xstring option parser
+  val target: (xstring * Position.T) parser
+  val opt_target: (xstring * Position.T) option parser
 end;
 
 structure Parse: PARSE =
@@ -362,7 +362,7 @@
 
 (* targets *)
 
-val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
+val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
 val opt_target = Scan.option target;
 
 end;
diff -r ae60518ac054 -r 6d71d9e52369 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Nov 14 16:24:50 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Nov 14 16:52:19 2011 +0100
@@ -58,14 +58,16 @@
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
-  val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
+  val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
+    transition -> transition
+  val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
     transition -> transition
-  val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
-  val present_local_theory: xstring option -> (state -> unit) -> transition -> transition
-  val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
+  val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
     transition -> transition
-  val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
-    transition -> transition
+  val local_theory_to_proof': (xstring * Position.T) option ->
+    (bool -> local_theory -> Proof.state) -> transition -> transition
+  val local_theory_to_proof: (xstring * Position.T) option ->
+    (local_theory -> Proof.state) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   val forget_proof: transition -> transition
@@ -105,7 +107,7 @@
 val loc_init = Named_Target.context_cmd;
 val loc_exit = Local_Theory.exit_global;
 
-fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
+fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy
   | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;