merged

--- a/Admin/polyml/build	Mon Mar 12 16:14:25 2012 +0000
+++ b/Admin/polyml/build	Mon Mar 12 16:57:29 2012 +0000
@@ -51,14 +51,14 @@
     OPTIONS=()
     ;;
   x86-darwin)
-    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
-      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3'
+    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include'
+      CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3'
       LDFLAGS='-segprot POLY rwx rwx')
     ;;
   x86_64-darwin)
-    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
-      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64'
-      LDFLAGS='-segprot POLY rwx rwx')
+   OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include'
+     CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64'
+     LDFLAGS='-segprot POLY rwx rwx')
     ;;
   x86-cygwin)
     OPTIONS=()

--- a/src/Provers/classical.ML	Mon Mar 12 16:14:25 2012 +0000
+++ b/src/Provers/classical.ML	Mon Mar 12 16:57:29 2012 +0000
@@ -301,9 +301,9 @@
     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   else Tactic.make_elim th;
 
-fun warn_thm context msg th =
-  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
-  then warning (msg ^ string_of_thm context th)
+fun warn_thm opt_context msg th =
+  if (case opt_context of SOME context => Context_Position.is_visible_proof context | NONE => false)
+  then warning (msg ^ string_of_thm opt_context th)
   else ();
 
 fun warn_rules context msg rules th =

--- a/src/Pure/Isar/outer_syntax.ML	Mon Mar 12 16:14:25 2012 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 12 16:57:29 2012 +0000
@@ -34,7 +34,7 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
-  val read_command: Position.T -> string -> Toplevel.transition
+  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
 end;
@@ -270,12 +270,6 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun read_command pos str =
-  let
-    val (lexs, outer_syntax) = get_syntax ();
-    val toks = Thy_Syntax.parse_tokens lexs pos str;
-  in #1 (read_span outer_syntax toks) end;
-
 fun read_element outer_syntax init {head, proof, proper_proof} =
   let
     val read = read_span outer_syntax o Thy_Syntax.span_content;

--- a/src/Pure/PIDE/document.ML	Mon Mar 12 16:14:25 2012 +0000
+++ b/src/Pure/PIDE/document.ML	Mon Mar 12 16:57:29 2012 +0000
@@ -240,7 +240,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
+  commands: (string * Token.T list future) Inttab.table,  (*command_id -> name * span*)
   execution: version_id * Future.group}  (*current execution process*)
 with
 
@@ -273,17 +273,18 @@
 
 (* commands *)
 
+fun tokenize_command id text =
+  Position.setmp_thread_data (Position.id_only id)
+    (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) ();
+
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val id_string = print_id id;
       val future =
         (singleton o Future.forks)
           {name = "Document.define_command", group = SOME (Future.new_group NONE),
             deps = [], pri = ~1, interrupts = false}
-          (fn () =>
-            Position.setmp_thread_data (Position.id_only id_string)
-              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
+          (fn () => tokenize_command (print_id id) text);
       val commands' =
         Inttab.update_new (id, (name, future)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -408,16 +409,20 @@
   if bad_init andalso is_none init then NONE
   else
     let
-      val (name, tr0) = the_command state command_id' ||> Future.join;
+      val (name, span) = the_command state command_id' ||> Future.join;
       val (modify_init, init') =
         if Keyword.is_theory_begin name then
           (Toplevel.modify_init (the_default illegal_init init), NONE)
         else (I, init);
       val exec_id' = new_id ();
-      val tr = tr0
-        |> modify_init
-        |> Toplevel.put_id (print_id exec_id');
-      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command tr st);
+      val exec_id'_string = print_id exec_id';
+      val tr =
+        Position.setmp_thread_data (Position.id_only exec_id'_string)
+          (fn () =>
+            #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+            |> modify_init
+            |> Toplevel.put_id exec_id'_string);
+      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 

--- a/src/Pure/context_position.ML	Mon Mar 12 16:14:25 2012 +0000
+++ b/src/Pure/context_position.ML	Mon Mar 12 16:57:29 2012 +0000
@@ -10,6 +10,7 @@
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
+  val is_visible_proof: Context.generic -> bool
   val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
@@ -27,8 +28,10 @@
 
 fun if_visible ctxt f x = if is_visible ctxt then f x else ();
 
-fun if_visible_proof (Context.Proof ctxt) f x = if_visible ctxt f x
-  | if_visible_proof _ _ _ = ();
+fun is_visible_proof (Context.Proof ctxt) = is_visible ctxt
+  | is_visible_proof _ = false;
+
+fun if_visible_proof context f x = if is_visible_proof context then f x else ();
 
 fun reported_text ctxt pos markup txt =
   if is_visible ctxt then Position.reported_text pos markup txt else "";

--- a/src/Pure/type_infer_context.ML	Mon Mar 12 16:14:25 2012 +0000
+++ b/src/Pure/type_infer_context.ML	Mon Mar 12 16:57:29 2012 +0000
@@ -118,18 +118,14 @@
 
 fun prepare_positions ctxt tms =
   let
-    val visible = Context_Position.is_visible ctxt;
-
     fun prepareT (Type (a, Ts)) ps_idx =
           let val (Ts', ps_idx') = fold_map prepareT Ts ps_idx
           in (Type (a, Ts'), ps_idx') end
       | prepareT T (ps, idx) =
           (case Term_Position.decode_positionT T of
             SOME pos =>
-              if visible then
-                let val U = Type_Infer.mk_param idx []
-                in (U, ((pos, U) :: ps, idx + 1)) end
-              else (dummyT, (ps, idx))
+              let val U = Type_Infer.mk_param idx []
+              in (U, ((pos, U) :: ps, idx + 1)) end
           | NONE => (T, (ps, idx)));
 
     fun prepare (Const ("_type_constraint_", T)) ps_idx =