# HG changeset patch
# User huffman
# Date 1314139613 25200
# Node ID f8c2def19f8422a91e0a4a2ef80fbec42a1d030e
# Parent  d366fa5551eff1511156991fac2ffb0774d3b4ee# Parent  d848dd7b21f4c1e9da9fe4e2ed3a03de3eca26c7
merged

diff -r d366fa5551ef -r f8c2def19f84 src/HOL/HOLCF/IOA/ABP/Check.ML
--- a/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -112,21 +112,21 @@
    ------------------------------------*)
 
 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
-  let fun prec x = (Output.raw_stdout ","; pre x)
+  let fun prec x = (Output.physical_stdout ","; pre x)
   in
     (case lll of
-      [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
-    | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
+      [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
+    | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
    end;
 
-fun pr_bool true = Output.raw_stdout "true"
-|   pr_bool false = Output.raw_stdout "false";
+fun pr_bool true = Output.physical_stdout "true"
+|   pr_bool false = Output.physical_stdout "false";
 
-fun pr_msg m = Output.raw_stdout "m"
-|   pr_msg n = Output.raw_stdout "n"
-|   pr_msg l = Output.raw_stdout "l";
+fun pr_msg m = Output.physical_stdout "m"
+|   pr_msg n = Output.physical_stdout "n"
+|   pr_msg l = Output.physical_stdout "l";
 
-fun pr_act a = Output.raw_stdout (case a of
+fun pr_act a = Output.physical_stdout (case a of
       Next => "Next"|                         
       S_msg(ma) => "S_msg(ma)"  |
       R_msg(ma) => "R_msg(ma)"  |
@@ -135,17 +135,17 @@
       S_ack(b)   => "S_ack(b)" |                      
       R_ack(b)   => "R_ack(b)");
 
-fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
+fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_stdout ">");
 
 val pr_bool_list  = print_list("[","]",pr_bool);
 val pr_msg_list   = print_list("[","]",pr_msg);
 val pr_pkt_list   = print_list("[","]",pr_pkt);
 
 fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
-        (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
-         pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
-         pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
-         pr_bool_list ch2; Output.raw_stdout "}");
+        (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p;  Output.physical_stdout ", ";
+         pr_bool a;  Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
+         pr_bool b;  Output.physical_stdout ", "; pr_pkt_list ch1;  Output.physical_stdout ", ";
+         pr_bool_list ch2; Output.physical_stdout "}");
 
 
 
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Library/FuncSet.thy	Tue Aug 23 15:46:53 2011 -0700
@@ -72,7 +72,7 @@
   by (auto simp: Pi_def)
 
 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
-  by (auto intro: Pi_I)
+  by auto
 
 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
   by (simp add: Pi_def)
@@ -257,7 +257,7 @@
 where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
 
 lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
-unfolding extensional_def by (auto intro: ext)
+unfolding extensional_def by auto
 
 lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
 unfolding extensional_funcset_def by simp
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -15,11 +15,14 @@
 val e_weight_methodK = "e_weight_method"
 val force_sosK = "force_sos"
 val max_relevantK = "max_relevant"
+val max_callsK = "max_calls"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
 val metis_ftK = "metis_ft"
 val reconstructorK = "reconstructor"
 
+val preplay_timeout = "4"
+
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
 fun reconstructor_tag reconstructor id =
@@ -361,7 +364,7 @@
     fun set_file_name (SOME dir) =
         Config.put Sledgehammer_Provers.dest_dir dir
         #> Config.put Sledgehammer_Provers.problem_prefix
-          ("prob_" ^ str0 (Position.line_of pos))
+          ("prob_" ^ str0 (Position.line_of pos) ^ "__")
         #> Config.put SMT_Config.debug_files
           (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
           ^ serial_string ())
@@ -376,15 +379,18 @@
                        e_weight_method |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.force_sos)
                        force_sos |> the_default I)
-                 #> Config.put Sledgehammer_Provers.measure_run_time true)
+                 #> Config.put Sledgehammer_Provers.measure_run_time true
+                 #> Config.put Sledgehammer_Provers.atp_sound_modulo_infiniteness false)
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_enc", type_enc),
            ("sound", sound),
+           ("preplay_timeout", preplay_timeout),
            ("max_relevant", max_relevant),
            ("slicing", slicing),
-           ("timeout", string_of_int timeout)]
+           ("timeout", string_of_int timeout),
+           ("preplay_timeout", preplay_timeout)]
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
         prover_name
@@ -520,7 +526,8 @@
        ("verbose", "true"),
        ("type_enc", type_enc),
        ("sound", sound),
-       ("timeout", string_of_int timeout)]
+       ("timeout", string_of_int timeout),
+       ("preplay_timeout", preplay_timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
@@ -543,6 +550,20 @@
   end
 
 
+val e_override_params =
+  [("provers", "e"),
+   ("max_relevant", "0"),
+   ("type_enc", "poly_guards?"),
+   ("sound", "true"),
+   ("slicing", "false")]
+
+val vampire_override_params =
+  [("provers", "vampire"),
+   ("max_relevant", "0"),
+   ("type_enc", "poly_tags"),
+   ("sound", "true"),
+   ("slicing", "false")]
+
 fun run_reconstructor trivial full m name reconstructor named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
@@ -550,15 +571,21 @@
       (if !reconstructor = "sledgehammer_tac" then
          (fn ctxt => fn thms =>
             Method.insert_tac thms THEN'
-            Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+            (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+                 e_override_params
+             ORELSE'
+             Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+                 vampire_override_params))
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metis (full_types)" then
          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc]
        else if !reconstructor = "metis (no_types)" then
          Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
+       else if !reconstructor = "metis" then
+         Metis_Tactics.metis_tac []
        else
-         Metis_Tactics.metis_tac []) ctxt thms
+         K (K (K all_tac))) ctxt thms
     fun apply_reconstructor thms =
       Mirabelle.can_apply timeout (do_reconstructor thms) st
 
@@ -591,48 +618,60 @@
 
 val try_timeout = seconds 5.0
 
+(* crude hack *)
+val num_sledgehammer_calls = Unsynchronized.ref 0
+
 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
   let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
     if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
     then () else
     let
-      val reconstructor = Unsynchronized.ref ""
-      val named_thms =
-        Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
-      val minimize = AList.defined (op =) args minimizeK
-      val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial =
-        Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
-        handle TimeLimit.TimeOut => false
-      fun apply_reconstructor m1 m2 =
-        if metis_ft
-        then
-          if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-              (run_reconstructor trivial false m1 name reconstructor
-                   (these (!named_thms))) id st)
+      val max_calls =
+        AList.lookup (op =) args max_callsK |> the_default "10000000"
+        |> Int.fromString |> the
+      val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1;
+    in
+      if !num_sledgehammer_calls > max_calls then ()
+      else
+        let
+          val reconstructor = Unsynchronized.ref ""
+          val named_thms =
+            Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
+          val minimize = AList.defined (op =) args minimizeK
+          val metis_ft = AList.defined (op =) args metis_ftK
+          val trivial =
+            Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
+            handle TimeLimit.TimeOut => false
+          fun apply_reconstructor m1 m2 =
+            if metis_ft
+            then
+              if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+                  (run_reconstructor trivial false m1 name reconstructor
+                       (these (!named_thms))) id st)
+              then
+                (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+                  (run_reconstructor trivial true m2 name reconstructor
+                       (these (!named_thms))) id st; ())
+              else ()
+            else
+              (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+                (run_reconstructor trivial false m1 name reconstructor
+                     (these (!named_thms))) id st; ())
+        in
+          change_data id (set_mini minimize);
+          Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
+                                                   named_thms) id st;
+          if is_some (!named_thms)
           then
-            (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-              (run_reconstructor trivial true m2 name reconstructor
-                   (these (!named_thms))) id st; ())
+           (apply_reconstructor Unminimized UnminimizedFT;
+            if minimize andalso not (null (these (!named_thms)))
+            then
+             (Mirabelle.catch minimize_tag
+                  (run_minimize args reconstructor named_thms) id st;
+              apply_reconstructor Minimized MinimizedFT)
+            else ())
           else ()
-        else
-          (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-            (run_reconstructor trivial false m1 name reconstructor
-                 (these (!named_thms))) id st; ())
-    in 
-      change_data id (set_mini minimize);
-      Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
-                                               named_thms) id st;
-      if is_some (!named_thms)
-      then
-       (apply_reconstructor Unminimized UnminimizedFT;
-        if minimize andalso not (null (these (!named_thms)))
-        then
-         (Mirabelle.catch minimize_tag
-              (run_minimize args reconstructor named_thms) id st;
-          apply_reconstructor Minimized MinimizedFT)
-        else ())
-      else ()
+        end
     end
   end
 
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/TPTP/CASC_Setup.thy
--- a/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 15:46:53 2011 -0700
@@ -119,14 +119,14 @@
    SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
-       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
-       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "metis"
        (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -270,7 +270,7 @@
 (* SPASS *)
 
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
-   counteracting the presence of "hAPP". *)
+   counteracting the presence of explicit application operators. *)
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
@@ -334,12 +334,13 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
      (if is_old_vampire_version () then
-        [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+        [(0.333, (false, (150, FOF, "poly_guards", sosN))),
+         (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
          (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
       else
-        [(0.334, (true, (50, TFF, "simple", no_sosN))),
+        [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+         (0.334, (true, (50, TFF, "simple", no_sosN))),
          (0.333, (false, (500, TFF, "simple", sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -165,8 +165,8 @@
 val untyped_helper_suffix = "_U"
 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
 
-val predicator_name = "hBOOL"
-val app_op_name = "hAPP"
+val predicator_name = "p"
+val app_op_name = "a"
 val type_guard_name = "g"
 val type_tag_name = "t"
 val simple_type_prefix = "ty_"
@@ -1151,7 +1151,7 @@
       | homo _ _ = raise Fail "expected function type"
   in homo end
 
-(** "hBOOL" and "hAPP" **)
+(** predicators and application operators **)
 
 type sym_info =
   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
@@ -1194,6 +1194,8 @@
            if String.isPrefix bound_var_prefix s orelse
               String.isPrefix all_bound_var_prefix s then
              add_universal_var T accum
+           else if String.isPrefix exist_bound_var_prefix s then
+             accum
            else
              let val ary = length args in
                ((bool_vars, fun_var_Ts),
@@ -1238,8 +1240,8 @@
       end
   in add true end
 fun add_fact_syms_to_table ctxt explicit_apply =
-  fact_lift (formula_fold NONE
-                          (K (add_iterm_syms_to_table ctxt explicit_apply)))
+  formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply))
+  |> fact_lift
 
 val tvar_a = TVar (("'a", 0), HOLogic.typeS)
 
@@ -1379,6 +1381,9 @@
 
 (** Helper facts **)
 
+val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
+val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
+
 (* The Boolean indicates that a fairly sound type encoding is needed. *)
 val helper_table =
   [(("COMBI", false), @{thms Meson.COMBI_def}),
@@ -1386,9 +1391,10 @@
    (("COMBB", false), @{thms Meson.COMBB_def}),
    (("COMBC", false), @{thms Meson.COMBC_def}),
    (("COMBS", false), @{thms Meson.COMBS_def}),
-   (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
+   ((predicator_name, false), [not_ffalse, ftrue]),
+   (("fFalse", false), [not_ffalse]),
    (("fFalse", true), @{thms True_or_False}),
-   (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
+   (("fTrue", false), [ftrue]),
    (("fTrue", true), @{thms True_or_False}),
    (("fNot", false),
     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
@@ -1754,9 +1760,7 @@
   (case type_enc of
      Guards _ => not pred_sym
    | _ => true) andalso
-  is_tptp_user_symbol s andalso
-  forall (fn prefix => not (String.isPrefix prefix s))
-         [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix]
+  is_tptp_user_symbol s
 
 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
                              (conjs, facts) =
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/ex/Unification.thy	Tue Aug 23 15:46:53 2011 -0700
@@ -11,10 +11,10 @@
 begin
 
 text {* 
-  Implements Manna & Waldinger's formalization, with Paulson's
+  Implements Manna \& Waldinger's formalization, with Paulson's
   simplifications, and some new simplifications by Slind and Krauss.
 
-  Z Manna & R Waldinger, Deductive Synthesis of the Unification
+  Z Manna \& R Waldinger, Deductive Synthesis of the Unification
   Algorithm.  SCP 1 (1981), 5-48
 
   L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
diff -r d366fa5551ef -r f8c2def19f84 src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -7,22 +7,21 @@
 
 signature SLEDGEHAMMER_TACTICS =
 sig
-  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
-  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
-  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+  val sledgehammer_with_metis_tac :
+    Proof.context -> (string * string) list -> int -> tactic
+  val sledgehammer_as_oracle_tac :
+    Proof.context -> (string * string) list -> int -> tactic
 end;
 
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
 struct
 
-fun run_atp force_full_types timeout i n ctxt goal name =
+fun run_atp override_params i n ctxt goal =
   let
     val chained_ths = [] (* a tactic has no chained ths *)
-    val params as {relevance_thresholds, max_relevant, slicing, ...} =
-      ((if force_full_types then [("sound", "true")] else [])
-       @ [("timeout", string_of_int (Time.toSeconds timeout))])
-       (* @ [("overlord", "true")] *)
-      |> Sledgehammer_Isar.default_params ctxt
+    val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
+      Sledgehammer_Isar.default_params ctxt override_params
+    val name = hd provers
     val prover =
       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
     val default_max_relevant =
@@ -50,8 +49,6 @@
       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end
 
-val atp = "e" (* or "vampire" or "spass" etc. *)
-
 fun thms_of_name ctxt name =
   let
     val lex = Keyword.get_lexicons
@@ -65,25 +62,16 @@
     |> Source.exhaust
   end
 
-fun sledgehammer_with_metis_tac ctxt i th =
-  let
-    val timeout = Time.fromSeconds 30
-  in
-    case run_atp false timeout i i ctxt th atp of
-      SOME facts =>
-      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
-    | NONE => Seq.empty
-  end
+fun sledgehammer_with_metis_tac ctxt override_params i th =
+  case run_atp override_params i i ctxt th of
+    SOME facts =>
+    Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
+  | NONE => Seq.empty
 
-fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
+fun sledgehammer_as_oracle_tac ctxt override_params i th =
   let
     val thy = Proof_Context.theory_of ctxt
-    val timeout = Time.fromSeconds 30
-    val xs = run_atp force_full_types timeout i i ctxt th atp
+    val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
 
-val sledgehammer_as_unsound_oracle_tac =
-  generic_sledgehammer_as_oracle_tac false
-val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
-
 end;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -51,13 +51,12 @@
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> task list
   val cancel: 'a future -> task list
-  type fork_params =
-    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
-  val forks: fork_params -> (unit -> 'a) list -> 'a future list
+  type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
+  val default_params: params
+  val forks: params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
@@ -67,7 +66,7 @@
   val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
-  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
+  val cond_forks: params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
   val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
@@ -125,11 +124,6 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished future evaluation");
-
 
 
 (** scheduling **)
@@ -464,10 +458,10 @@
 
 (* fork *)
 
-type fork_params =
-  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
 
-fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
+fun forks ({name, group, deps, pri, interrupts}: params) es =
   if null es then []
   else
     let
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/lazy.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -11,11 +11,12 @@
   type 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
   val is_finished: 'a lazy -> bool
-  val get_finished: 'a lazy -> 'a
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
+  val map: ('a -> 'b) -> 'a lazy -> 'b lazy
+  val future: Future.params -> 'a lazy -> 'a future
 end;
 
 structure Lazy: LAZY =
@@ -40,11 +41,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)
 
@@ -77,9 +73,19 @@
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
         end) ());
 
-fun force r = Exn.release (force_result r);
 
 end;
+
+fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+  if is_finished x then Future.value_result (force_result x)
+  else (singleton o Future.forks) params (fn () => force x);
+
 end;
 
 type 'a lazy = 'a Lazy.lazy;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -27,11 +27,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)
 
@@ -45,6 +40,14 @@
   in result end;
 
 fun force r = Exn.release (force_result r);
+fun map f x = lazy (fn () => f (force x));
+
+
+(* future evaluation *)
+
+fun future params x =
+  if is_finished x then Future.value_result (force_result x)
+  else (singleton o Future.forks) params (fn () => force x);
 
 end;
 end;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/General/output.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -22,9 +22,9 @@
   val output_width: string -> output * int
   val output: string -> output
   val escape: output -> string
-  val raw_stdout: output -> unit
-  val raw_stderr: output -> unit
-  val raw_writeln: output -> unit
+  val physical_stdout: output -> unit
+  val physical_stderr: output -> unit
+  val physical_writeln: output -> unit
   structure Private_Hooks:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -78,24 +78,24 @@
 
 (* raw output primitives -- not to be used in user-space *)
 
-fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
 
-fun raw_writeln "" = ()
-  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
+fun physical_writeln "" = ()
+  | physical_writeln s = physical_stdout (suffix "\n" s);  (*atomic output!*)
 
 
 (* Isabelle output channels *)
 
 structure Private_Hooks =
 struct
-  val writeln_fn = Unsynchronized.ref raw_writeln;
+  val writeln_fn = Unsynchronized.ref physical_writeln;
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+  val warning_fn = Unsynchronized.ref (physical_stdout o suffix "\n" o prefix_lines "### ");
   val error_fn =
-    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
-  val prompt_fn = Unsynchronized.ref raw_stdout;
+    Unsynchronized.ref (fn (_: serial, s) => physical_stdout (suffix "\n" (prefix_lines "*** " s)));
+  val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
   val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/command.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -84,6 +84,19 @@
 
   def span(toks: List[Token]): Command =
     new Command(Document.no_id, toks)
+
+
+  /* perspective */
+
+  type Perspective = List[Command]  // visible commands in canonical order
+
+  def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+  {
+    require(p1.forall(_.is_defined))
+    require(p2.forall(_.is_defined))
+    p1.length == p2.length &&
+      (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+  }
 }
 
 
@@ -93,12 +106,12 @@
 {
   /* classification */
 
+  def is_defined: Boolean = id != Document.no_id
+
   def is_command: Boolean = !span.isEmpty && span.head.is_command
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
-  def is_unparsed = id == Document.no_id
-
   def name: String = if (is_command) span.head.content else ""
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/document.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -19,7 +19,8 @@
   datatype node_edit =
     Clear |
     Edits of (command_id option * command_id option) list |
-    Header of node_header
+    Header of node_header |
+    Perspective of command_id list
   type edit = string * node_edit
   type state
   val init_state: state
@@ -56,34 +57,54 @@
 (** document structure **)
 
 type node_header = (string * string list * (string * bool) list) Exn.result;
+type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
  {header: node_header,
+  perspective: perspective,
   entries: exec_id option Entries.T,  (*command entries with excecutions*)
   result: Toplevel.state lazy}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, entries, result) =
-  Node {header = header, entries = entries, result = result};
+fun make_node (header, perspective, entries, result) =
+  Node {header = header, perspective = perspective, entries = entries, result = result};
+
+fun map_node f (Node {header, perspective, entries, result}) =
+  make_node (f (header, perspective, entries, result));
 
-fun map_node f (Node {header, entries, result}) =
-  make_node (f (header, entries, result));
+val no_perspective: perspective = (K false, []);
+val no_print = Lazy.value ();
+val no_result = Lazy.value Toplevel.toplevel;
+
+val empty_node =
+  make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
+
+val clear_node =
+  map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+
+
+(* basic components *)
 
 fun get_header (Node {header, ...}) = header;
-fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
+fun set_header header =
+  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
 
-fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
+fun get_perspective (Node {perspective, ...}) = perspective;
+fun set_perspective perspective =
+  let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in
+    map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result))
+  end;
+
+fun map_entries f (Node {header, perspective, entries, result}) =
+  make_node (header, perspective, f entries, result);
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
-fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
-fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
-
-val empty_exec = Lazy.value Toplevel.toplevel;
-val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
-val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
+fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
+fun set_result result =
+  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
 
 fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
 fun default_node name = Graph.default_node (name, empty_node);
@@ -95,7 +116,8 @@
 datatype node_edit =
   Clear |
   Edits of (command_id option * command_id option) list |
-  Header of node_header;
+  Header of node_header |
+  Perspective of command_id list;
 
 type edit = string * node_edit;
 
@@ -150,7 +172,9 @@
             val (header', nodes3) =
               (header, Graph.add_deps_acyclic (name, parents) nodes2)
                 handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
-          in Graph.map_node name (set_header header') nodes3 end));
+          in Graph.map_node name (set_header header') nodes3 end
+      | Perspective perspective =>
+          update_node name (set_perspective perspective) nodes));
 
 fun put_node (name, node) (Version nodes) =
   Version (update_node name (K node) nodes);
@@ -164,7 +188,8 @@
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
-  execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
+  execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
+    (*exec_id -> command_id with eval/print process*)
   execution: Future.group}  (*global execution process*)
 with
 
@@ -177,7 +202,7 @@
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
-    Inttab.make [(no_id, empty_exec)],
+    Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
     Future.new_group NONE);
 
 
@@ -252,14 +277,9 @@
     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun async_state tr st =
-  (singleton o Future.forks)
-    {name = "Document.async_state", group = SOME (Future.new_group NONE),
-      deps = [], pri = 0, interrupts = true}
-    (fn () =>
-      Toplevel.setmp_thread_position tr
-        (fn () => Toplevel.print_state false st) ())
-  |> ignore;
+fun print_state tr st =
+  (Lazy.lazy o Toplevel.setmp_thread_position tr)
+    (fn () => Toplevel.print_state false st);
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -286,12 +306,11 @@
     val _ = List.app (Toplevel.error_msg tr) errs;
   in
     (case result of
-      NONE => (Toplevel.status tr Markup.failed; st)
+      NONE => (Toplevel.status tr Markup.failed; (st, no_print))
     | SOME st' =>
        (Toplevel.status tr Markup.finished;
         proof_status tr st';
-        if do_print then async_state tr st' else ();
-        st'))
+        (st', if do_print then print_state tr st' else no_print)))
   end;
 
 end;
@@ -313,13 +332,10 @@
 fun new_exec (command_id, command) (assigns, execs, exec) =
   let
     val exec_id' = new_id ();
-    val exec' =
-      Lazy.lazy (fn () =>
-        let
-          val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
-          val st = Lazy.get_finished exec;
-        in run_command tr st end);
-  in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
+    val exec' = exec |> Lazy.map (fn (st, _) =>
+      let val tr = Toplevel.put_id (print_id exec_id') (Future.join command)
+      in run_command tr st end);
+  in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
 
 in
 
@@ -351,7 +367,7 @@
                         | NONE =>
                             get_theory (Position.file_only import)
                               (#2 (Future.join (the (AList.lookup (op =) deps import))))));
-                  in Thy_Load.begin_theory dir thy_name imports files parents end
+                  in Thy_Load.begin_theory dir thy_name imports files parents end;
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));
               in
@@ -364,12 +380,12 @@
                         (case prev of
                           NONE => no_id
                         | SOME prev_id => the_default no_id (the_entry node prev_id));
-                      val (assigns, execs, result) =
+                      val (assigns, execs, last_exec) =
                         fold_entries (SOME id) (new_exec o get_command o #2 o #1)
-                          node ([], [], the_exec state prev_exec);
+                          node ([], [], #2 (the_exec state prev_exec));
                       val node' = node
                         |> fold update_entry assigns
-                        |> set_result result;
+                        |> set_result (Lazy.map #1 last_exec);
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
       |> Future.joins |> map #1;
@@ -390,8 +406,17 @@
     let
       val version = the_version state version_id;
 
-      fun force_exec NONE = ()
-        | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
+      fun force_exec _ NONE = ()
+        | force_exec node (SOME exec_id) =
+            let
+              val (command_id, exec) = the_exec state exec_id;
+              val (_, print) = Lazy.force exec;
+              val perspective = get_perspective node;
+              val _ =
+                if #1 (get_perspective node) command_id orelse true  (* FIXME *)
+                then ignore (Lazy.future Future.default_params print)
+                else ();
+            in () end;
 
       val execution = Future.new_group NONE;
       val _ =
@@ -400,7 +425,7 @@
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
-              (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
+              (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
 
     in (versions, commands, execs, execution) end);
 
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/document.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -31,35 +31,37 @@
 
   /* named nodes -- development graph */
 
-  type Edit[A] = (String, Node.Edit[A])
-  type Edit_Text = Edit[Text.Edit]
-  type Edit_Command = Edit[(Option[Command], Option[Command])]
-  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
+  type Edit[A, B] = (String, Node.Edit[A, B])
+  type Edit_Text = Edit[Text.Edit, Text.Perspective]
+  type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
   type Node_Header = Exn.Result[Thy_Header]
 
   object Node
   {
-    sealed abstract class Edit[A]
+    sealed abstract class Edit[A, B]
     {
-      def map[B](f: A => B): Edit[B] =
+      def foreach(f: A => Unit)
+      {
         this match {
-          case Clear() => Clear()
-          case Edits(es) => Edits(es.map(f))
-          case Header(header) => Header(header)
+          case Edits(es) => es.foreach(f)
+          case _ =>
         }
+      }
     }
-    case class Clear[A]() extends Edit[A]
-    case class Edits[A](edits: List[A]) extends Edit[A]
-    case class Header[A](header: Node_Header) extends Edit[A]
+    case class Clear[A, B]() extends Edit[A, B]
+    case class Edits[A, B](edits: List[A]) extends Edit[A, B]
+    case class Header[A, B](header: Node_Header) extends Edit[A, B]
+    case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
-    def norm_header[A](f: String => String, g: String => String, header: Node_Header): Header[A] =
+    def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
+        : Header[A, B] =
       header match {
-        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f, g) })
-        case exn => Header[A](exn)
+        case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
+        case exn => Header[A, B](exn)
       }
 
-    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
+    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -77,6 +79,7 @@
 
   sealed case class Node(
     val header: Node_Header,
+    val perspective: Command.Perspective,
     val blobs: Map[String, Blob],
     val commands: Linear_Set[Command])
   {
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -27,7 +27,8 @@
                   fn ([], a) =>
                     Document.Header
                       (Exn.Res (triple string (list string) (list (pair string bool)) a)),
-                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
+                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+                  fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
       val running = Document.cancel_execution state;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -140,18 +140,20 @@
   /* document versions */
 
   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-    edits: List[Document.Edit_Command_ID])
+    edits: List[Document.Edit_Command])
   {
     val edits_yxml =
     { import XML.Encode._
-      def encode: T[List[Document.Edit_Command_ID]] =
+      def id: T[Command] = (cmd => long(cmd.id))
+      def encode: T[List[Document.Edit_Command]] =
         list(pair(string,
           variant(List(
             { case Document.Node.Clear() => (Nil, Nil) },
-            { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
+            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
                 (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
-            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
+            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
+            { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -22,10 +22,7 @@
     type Entry = (Text.Info[Any], Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
-    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
-      {
-        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
-      })
+    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
 
     def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
     def single(entry: Entry): T = update(empty, entry)
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/PIDE/text.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -8,6 +8,11 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.math.Ordering
+import scala.util.Sorting
+
+
 object Text
 {
   /* offset */
@@ -20,6 +25,11 @@
   object Range
   {
     def apply(start: Offset): Range = Range(start, start)
+
+    object Ordering extends scala.math.Ordering[Text.Range]
+    {
+      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
+    }
   }
 
   sealed case class Range(val start: Offset, val stop: Offset)
@@ -50,6 +60,33 @@
   }
 
 
+  /* perspective */
+
+  type Perspective = List[Range]  // visible text partitioning in canonical order
+
+  def perspective(ranges: Seq[Range]): Perspective =
+  {
+    val sorted_ranges = ranges.toArray
+    Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+    val result = new mutable.ListBuffer[Text.Range]
+    var last: Option[Text.Range] = None
+    for (range <- sorted_ranges)
+    {
+      last match {
+        case Some(last_range)
+        if ((last_range overlaps range) || last_range.stop == range.start) =>
+          last = Some(Text.Range(last_range.start, range.stop))
+        case _ =>
+          result ++= last
+          last = Some(range)
+      }
+    }
+    result ++= last
+    result.toList
+  }
+
+
   /* information associated with text range */
 
   sealed case class Info[A](val range: Text.Range, val info: A)
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -75,7 +75,7 @@
 fun message bg en prfx text =
   (case render text of
     "" => ()
-  | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
+  | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
  (Output.Private_Hooks.writeln_fn := message "" "" "";
@@ -85,7 +85,7 @@
   Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
   Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -66,7 +66,7 @@
 
 fun matching_pgip_id id = (id = ! pgip_id)
 
-val output_xml_fn = Unsynchronized.ref Output.raw_writeln
+val output_xml_fn = Unsynchronized.ref Output.physical_writeln
 fun output_xml s = ! output_xml_fn (XML.string_of s);
 
 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -1009,7 +1009,7 @@
 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
 
 local
-    val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
+    val pgip_output_channel = Unsynchronized.ref Output.physical_writeln
 in
 
 (* Set recipient for PGIP results *)
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -255,8 +255,19 @@
 fun struct_tr structs [Const ("_indexdefault", _)] =
       Syntax.free (the_struct structs 1)
   | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
-      Syntax.free (the_struct structs
-        (case Lexicon.read_nat s of SOME n => n | NONE => raise TERM ("struct_tr", [t])))
+      (case Lexicon.read_nat s of
+        SOME n =>
+          let
+            val x = the_struct structs n;
+            val advice =
+              " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+              (if n = 1 then " (may be omitted)" else "");
+            val _ =
+              legacy_feature
+                ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
+                  Position.str_of (Position.thread_data ()) ^ advice);
+          in Syntax.free x end
+      | NONE => raise TERM ("struct_tr", [t]))
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -171,7 +171,7 @@
 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
-    val _ = Output.raw_stdout Symbol.STX;
+    val _ = Output.physical_stdout Symbol.STX;
 
     val _ = quick_and_dirty := true;
     val _ = Goal.parallel_proofs := 0;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/session.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -107,7 +107,7 @@
           val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
             |> Real.fmt (StringCvt.FIX (SOME 2));
           val _ =
-            Output.raw_stderr ("Timing " ^ item ^ " (" ^
+            Output.physical_stderr ("Timing " ^ item ^ " (" ^
               string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
               Timing.message timing ^ ", factor " ^ factor ^ ")\n");
         in () end
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/System/session.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -164,10 +164,10 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Interrupt
-  private case class Init_Node(
-    name: String, master_dir: String, header: Document.Node_Header, text: String)
-  private case class Edit_Node(
-    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
+  private case class Init_Node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, text: String)
+  private case class Edit_Node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   private case class Change_Node(
     name: String,
     doc_edits: List[Document.Edit_Command],
@@ -183,7 +183,7 @@
     /* incoming edits */
 
     def handle_edits(name: String, master_dir: String,
-        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
+        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
     //{{{
     {
       val syntax = current_syntax()
@@ -196,7 +196,8 @@
         else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
       }
       def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
-      val norm_header = Document.Node.norm_header[Text.Edit](norm_import, norm_use, header)
+      val norm_header =
+        Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
 
       val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
@@ -229,22 +230,20 @@
         removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
-      def id_command(command: Command): Document.Command_ID =
+      def id_command(command: Command)
       {
         if (global_state().lookup_command(command.id).isEmpty) {
           global_state.change(_.define_command(command))
           prover.get.define_command(command.id, Symbol.encode(command.source))
         }
-        command.id
       }
-      val id_edits =
-        doc_edits map {
-          case (name, edit) =>
-            (name, edit.map({ case (c1, c2) => (c1.map(id_command), c2.map(id_command)) }))
-        }
+      doc_edits foreach {
+        case (_, edit) =>
+          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
+      }
 
       global_state.change(_.define_version(version, former_assignment))
-      prover.get.edit_version(previous.id, version.id, id_edits)
+      prover.get.edit_version(previous.id, version.id, doc_edits)
     }
     //}}}
 
@@ -337,14 +336,18 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
+        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
           // FIXME compare with existing node
           handle_edits(name, master_dir, header,
-            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
+            List(Document.Node.Clear(),
+              Document.Node.Edits(List(Text.Edit.insert(0, text))),
+              Document.Node.Perspective(perspective)))
           reply(())
 
-        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
-          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
+        case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
+          handle_edits(name, master_dir, header,
+            List(Document.Node.Edits(text_edits),
+              Document.Node.Perspective(perspective)))
           reply(())
 
         case change: Change_Node if prover.isDefined =>
@@ -372,9 +375,13 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
-  { session_actor !? Init_Node(name, master_dir, header, text) }
+  // FIXME simplify signature
+  def init_node(name: String, master_dir: String,
+    header: Document.Node_Header, perspective: Text.Perspective, text: String)
+  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
 
-  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
-  { session_actor !? Edit_Node(name, master_dir, header, edits) }
+  // FIXME simplify signature
+  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
+    perspective: Text.Perspective, edits: List[Text.Edit])
+  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
 }
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Thy/present.ML	Tue Aug 23 15:46:53 2011 -0700
@@ -289,7 +289,8 @@
       val documents =
         if doc = "" then []
         else if not (can File.check_dir document_path) then
-          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
+          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
+           else (); [])
         else read_variants doc_variants;
 
       val parent_index_path = Path.append Path.parent index_path;
@@ -403,14 +404,14 @@
         File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
         List.app finish_html thys;
         List.app (uncurry File.write) files;
-        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
+        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
         else ())
       else ();
 
     val _ =
       (case dump_prefix of NONE => () | SOME (cp, path) =>
        (prepare_sources cp path;
-        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
+        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
         else ()));
 
     val doc_paths =
@@ -421,7 +422,8 @@
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =
       if verbose then
-        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
+        doc_paths
+        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
       else ();
   in
     browser_info := empty_browser_info;
diff -r d366fa5551ef -r f8c2def19f84 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -97,6 +97,37 @@
 
 
 
+  /** command perspective **/
+
+  def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
+  {
+    if (perspective.isEmpty) Nil
+    else {
+      val result = new mutable.ListBuffer[Command]
+      @tailrec
+      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
+      {
+        (ranges, commands) match {
+          case (range :: more_ranges, (command, offset) #:: more_commands) =>
+            val command_range = command.range + offset
+            range compare command_range match {
+              case -1 => check_ranges(more_ranges, commands)
+              case 0 =>
+                result += command
+                check_ranges(ranges, more_commands)
+              case 1 => check_ranges(ranges, more_commands)
+            }
+          case _ =>
+        }
+      }
+      val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
+      check_ranges(perspective, node.command_range(perspective_range).toStream)
+      result.toList
+    }
+  }
+
+
+
   /** text edits **/
 
   def text_edits(
@@ -138,7 +169,7 @@
 
     @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
-      commands.iterator.find(_.is_unparsed) match {
+      commands.iterator.find(cmd => !cmd.is_defined) match {
         case Some(first_unparsed) =>
           val first =
             commands.reverse_iterator(first_unparsed).
@@ -210,6 +241,14 @@
             doc_edits += (name -> Document.Node.Header(header))
             nodes += (name -> node.copy(header = header))
           }
+
+        case (name, Document.Node.Perspective(text_perspective)) =>
+          val node = nodes(name)
+          val perspective = command_perspective(node, text_perspective)
+          if (!Command.equal_perspective(node.perspective, perspective)) {
+            doc_edits += (name -> Document.Node.Perspective(perspective))
+            nodes += (name -> node.copy(perspective = perspective))
+          }
       }
       (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     }
diff -r d366fa5551ef -r f8c2def19f84 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -60,10 +60,29 @@
 class Document_Model(val session: Session, val buffer: Buffer,
   val master_dir: String, val node_name: String, val thy_name: String)
 {
-  /* pending text edits */
+  /* header */
 
   def node_header(): Exn.Result[Thy_Header] =
+  {
+    Swing_Thread.require()
     Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
+  }
+
+
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        doc_view <- Isabelle.document_views(buffer)
+        range <- doc_view.perspective()
+      } yield range)
+  }
+
+
+  /* pending text edits */
 
   private object pending_edits  // owned by Swing thread
   {
@@ -77,14 +96,15 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(node_name, master_dir, node_header(), edits)
+          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
+      session.init_node(node_name, master_dir,
+        node_header(), perspective(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
diff -r d366fa5551ef -r f8c2def19f84 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -10,6 +10,7 @@
 
 import isabelle._
 
+import scala.collection.mutable
 import scala.actors.Actor._
 
 import java.lang.System
@@ -86,7 +87,7 @@
   }
 
 
-  /* visible line ranges */
+  /* visible text range */
 
   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
   // NB: jEdit already normalizes \r\n and \r to \n
@@ -96,14 +97,14 @@
     Text.Range(start, stop)
   }
 
-  def screen_lines_range(): Text.Range =
+  def visible_range(): Text.Range =
   {
     val start = text_area.getScreenLineStartOffset(0)
     val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
     proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   }
 
-  def invalidate_line_range(range: Text.Range)
+  def invalidate_range(range: Text.Range)
   {
     text_area.invalidateLineRange(
       model.buffer.getLineOfOffset(range.start),
@@ -111,6 +112,22 @@
   }
 
 
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        i <- 0 until text_area.getVisibleLines
+        val start = text_area.getScreenLineStartOffset(i)
+        val stop = text_area.getScreenLineEndOffset(i)
+        if start >= 0 && stop >= 0
+      }
+      yield Text.Range(start, stop))
+  }
+
+
   /* snapshot */
 
   // owned by Swing thread
@@ -224,9 +241,9 @@
 
           if (control) init_popup(snapshot, x, y)
 
-          _highlight_range map { case (range, _) => invalidate_line_range(range) }
+          _highlight_range map { case (range, _) => invalidate_range(range) }
           _highlight_range = if (control) subexp_range(snapshot, x, y) else None
-          _highlight_range map { case (range, _) => invalidate_line_range(range) }
+          _highlight_range map { case (range, _) => invalidate_range(range) }
         }
     }
   }
@@ -415,15 +432,15 @@
           val buffer = model.buffer
           Isabelle.swing_buffer_lock(buffer) {
             val (updated, snapshot) = flush_snapshot()
-            val visible_range = screen_lines_range()
+            val visible = visible_range()
 
             if (updated || changed.exists(snapshot.node.commands.contains))
               overview.repaint()
 
-            if (updated) invalidate_line_range(visible_range)
+            if (updated) invalidate_range(visible)
             else {
               val visible_cmds =
-                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+                snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
               if (visible_cmds.exists(changed)) {
                 for {
                   line <- 0 until text_area.getVisibleLines
diff -r d366fa5551ef -r f8c2def19f84 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 23 14:11:02 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 23 15:46:53 2011 -0700
@@ -199,6 +199,13 @@
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
+  def document_views(buffer: Buffer): List[Document_View] =
+    for {
+      text_area <- jedit_text_areas(buffer).toList
+      val doc_view = document_view(text_area)
+      if doc_view.isDefined
+    } yield doc_view.get
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {