merged
authorwenzelm
Thu Mar 12 22:07:26 2015 +0100 (2015-03-12)
changeset 5968668996aa77829
parent 59681 f24ab09e4c37
parent 59685 c043306d2598
child 59687 3baf9b3a24c7
merged
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu Mar 12 19:09:18 2015 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Mar 12 22:07:26 2015 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  class) to a qualified member declaration:  @{text method}  *}
     1.5  
     1.6  definition
     1.7 -  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.8 +  "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.9    where "method sig m = (declclass m, mdecl (sig, mthd m))"
    1.10  
    1.11  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
     2.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 12 19:09:18 2015 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 12 22:07:26 2015 +0100
     2.3 @@ -429,14 +429,14 @@
     2.4    fixes G ("\<Gamma>") and Phi ("\<Phi>")
     2.5    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
     2.6    assumes is_class: "is_class \<Gamma> C"
     2.7 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     2.8 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     2.9      and m: "m \<noteq> init"
    2.10    defines start: "s \<equiv> start_state \<Gamma> C m"
    2.11  
    2.12    assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
    2.13    shows "t \<noteq> TypeError"
    2.14  proof -
    2.15 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.16 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.17      unfolding start by (rule BV_correct_initial)
    2.18    from wt this s show ?thesis by (rule no_type_errors)
    2.19  qed
    2.20 @@ -461,12 +461,12 @@
    2.21    fixes G ("\<Gamma>") and Phi ("\<Phi>")
    2.22    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
    2.23    assumes is_class: "is_class \<Gamma> C"
    2.24 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    2.25 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    2.26      and m: "m \<noteq> init"
    2.27    defines start: "s \<equiv> start_state \<Gamma> C m"
    2.28    shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
    2.29  proof -
    2.30 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.31 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.32      unfolding start by (rule BV_correct_initial)
    2.33    with wt show ?thesis by (rule welltyped_commutes)
    2.34  qed
     3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 12 19:09:18 2015 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 12 22:07:26 2015 +0100
     3.3 @@ -811,7 +811,7 @@
     3.4  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
     3.5  proof -
     3.6    assume wtprog: "wt_jvm_prog G phi"
     3.7 -  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     3.8 +  assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     3.9    assume ins:    "ins ! pc = Invoke C' mn pTs"
    3.10    assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    3.11    assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
    3.12 @@ -823,7 +823,7 @@
    3.13      wfprog: "wf_prog wfmb G" 
    3.14      by (simp add: wt_jvm_prog_def)
    3.15        
    3.16 -  from ins method approx
    3.17 +  from ins "method" approx
    3.18    obtain s where
    3.19      heap_ok: "G\<turnstile>h hp\<surd>" and
    3.20      prealloc:"preallocated hp" and
    3.21 @@ -880,7 +880,7 @@
    3.22    from stk' l_o l
    3.23    have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
    3.24  
    3.25 -  with state' method ins no_xcp oX_conf
    3.26 +  with state' "method" ins no_xcp oX_conf
    3.27    obtain ref where oX_Addr: "oX = Addr ref"
    3.28      by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
    3.29  
    3.30 @@ -922,7 +922,7 @@
    3.31        
    3.32    from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
    3.33  
    3.34 -  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
    3.35 +  with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
    3.36    have state'_val:
    3.37      "state' =
    3.38       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
    3.39 @@ -972,7 +972,7 @@
    3.40      show ?thesis by (simp add: correct_frame_def)
    3.41    qed
    3.42  
    3.43 -  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
    3.44 +  from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
    3.45         frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
    3.46    show ?thesis
    3.47      apply (simp add: correct_state_def)
     4.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Mar 12 19:09:18 2015 +0100
     4.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Mar 12 22:07:26 2015 +0100
     4.3 @@ -177,7 +177,7 @@
     4.4  qed
     4.5  
     4.6  consts
     4.7 -  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     4.8 +  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     4.9    field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    4.10    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    4.11  
     5.1 --- a/src/HOL/NanoJava/TypeRel.thy	Thu Mar 12 19:09:18 2015 +0100
     5.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Mar 12 22:07:26 2015 +0100
     5.3 @@ -108,7 +108,7 @@
     5.4  done
     5.5  
     5.6  --{* Methods of a class, with inheritance and hiding *}
     5.7 -definition method :: "cname => (mname \<rightharpoonup> methd)" where
     5.8 +definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
     5.9    "method C \<equiv> class_rec C methods"
    5.10  
    5.11  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
     6.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 19:09:18 2015 +0100
     6.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 22:07:26 2015 +0100
     6.3 @@ -284,7 +284,7 @@
     6.4      /* result structure */
     6.5  
     6.6      val spans = parse_spans(text)
     6.7 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
     6.8 +    spans.foreach(span => add(Command(Document_ID.none, node_name, None, span)))
     6.9      result()
    6.10    }
    6.11  }
     7.1 --- a/src/Pure/PIDE/command.ML	Thu Mar 12 19:09:18 2015 +0100
     7.2 +++ b/src/Pure/PIDE/command.ML	Thu Mar 12 22:07:26 2015 +0100
     7.3 @@ -51,21 +51,19 @@
     7.4  
     7.5  fun read_file_node file_node master_dir pos src_path =
     7.6    let
     7.7 -    val _ = Position.report pos Markup.language_path;
     7.8      val _ =
     7.9        (case try Url.explode file_node of
    7.10          NONE => ()
    7.11        | SOME (Url.File _) => ()
    7.12        | _ =>
    7.13 -         (Position.report pos (Markup.path file_node);
    7.14            error ("Prover cannot load remote file " ^
    7.15 -            Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
    7.16 +            Markup.markup (Markup.path file_node) (quote file_node)));
    7.17      val full_path = File.check_file (File.full_path master_dir src_path);
    7.18 -    val _ = Position.report pos (Markup.path (Path.implode full_path));
    7.19      val text = File.read full_path;
    7.20      val lines = split_lines text;
    7.21      val digest = SHA1.digest text;
    7.22 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
    7.23 +  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
    7.24 +  handle ERROR msg => error (msg ^ Position.here pos);
    7.25  
    7.26  val read_file = read_file_node "";
    7.27  
    7.28 @@ -89,8 +87,7 @@
    7.29                  Exn.interruptible_capture (fn () =>
    7.30                    read_file_node file_node master_dir pos src_path) ()
    7.31              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
    7.32 -               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
    7.33 -                Exn.Res (blob_file src_path lines digest file_node))
    7.34 +                Exn.Res (blob_file src_path lines digest file_node)
    7.35              | make_file _ (Exn.Exn e) = Exn.Exn e;
    7.36            val src_paths = Keyword.command_files keywords cmd path;
    7.37          in
     8.1 --- a/src/Pure/PIDE/command.scala	Thu Mar 12 19:09:18 2015 +0100
     8.2 +++ b/src/Pure/PIDE/command.scala	Thu Mar 12 22:07:26 2015 +0100
     8.3 @@ -253,15 +253,17 @@
     8.4    def apply(
     8.5      id: Document_ID.Command,
     8.6      node_name: Document.Node.Name,
     8.7 -    blobs: List[Blob],
     8.8 +    blobs: Option[(List[Blob], Int)],
     8.9      span: Command_Span.Span): Command =
    8.10    {
    8.11      val (source, span1) = span.compact_source
    8.12 -    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    8.13 +    val (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
    8.14 +    new Command(
    8.15 +      id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
    8.16    }
    8.17  
    8.18    val empty: Command =
    8.19 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
    8.20 +    Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
    8.21  
    8.22    def unparsed(
    8.23      id: Document_ID.Command,
    8.24 @@ -270,7 +272,7 @@
    8.25      markup: Markup_Tree): Command =
    8.26    {
    8.27      val (source1, span1) = Command_Span.unparsed(source).compact_source
    8.28 -    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    8.29 +    new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
    8.30    }
    8.31  
    8.32    def unparsed(source: String): Command =
    8.33 @@ -312,6 +314,7 @@
    8.34      val id: Document_ID.Command,
    8.35      val node_name: Document.Node.Name,
    8.36      val blobs: List[Command.Blob],
    8.37 +    val blobs_index: Int,
    8.38      val span: Command_Span.Span,
    8.39      val source: String,
    8.40      val init_results: Command.Results,
     9.1 --- a/src/Pure/PIDE/command_span.ML	Thu Mar 12 19:09:18 2015 +0100
     9.2 +++ b/src/Pure/PIDE/command_span.ML	Thu Mar 12 22:07:26 2015 +0100
     9.3 @@ -28,22 +28,20 @@
     9.4  
     9.5  local
     9.6  
     9.7 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
     9.8 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
     9.9 -      else (i1, t1) :: clean ((i2, t2) :: toks)
    9.10 +fun clean ((t1, i1) :: (t2, i2) :: rest) =
    9.11 +      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean rest
    9.12 +      else (t1, i1) :: clean ((t2, i2) :: rest)
    9.13    | clean toks = toks;
    9.14  
    9.15 -fun clean_tokens toks =
    9.16 -  ((0 upto length toks - 1) ~~ toks)
    9.17 -  |> filter (fn (_, tok) => Token.is_proper tok)
    9.18 -  |> clean;
    9.19 +fun clean_tokens tokens =
    9.20 +  clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
    9.21  
    9.22 -fun find_file ((_, tok) :: toks) =
    9.23 +fun find_file ((tok, _) :: toks) =
    9.24        if Token.is_command tok then
    9.25 -        toks |> get_first (fn (i, tok) =>
    9.26 -          if Token.is_name tok then
    9.27 -            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
    9.28 -              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
    9.29 +        toks |> get_first (fn (t, i) =>
    9.30 +          if Token.is_name t then
    9.31 +            SOME ((Path.explode (Token.content_of t), Token.pos_of t), i)
    9.32 +              handle ERROR msg => error (msg ^ Position.here (Token.pos_of t))
    9.33            else NONE)
    9.34        else NONE
    9.35    | find_file [] = NONE;
    9.36 @@ -56,7 +54,7 @@
    9.37        if Keyword.is_theory_load keywords cmd then
    9.38          (case find_file (clean_tokens toks) of
    9.39            NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    9.40 -        | SOME (i, path) =>
    9.41 +        | SOME (path, i) =>
    9.42              let
    9.43                val toks' = toks |> map_index (fn (j, tok) =>
    9.44                  if i = j then Token.put_files (read_files cmd path) tok
    10.1 --- a/src/Pure/PIDE/command_span.scala	Thu Mar 12 19:09:18 2015 +0100
    10.2 +++ b/src/Pure/PIDE/command_span.scala	Thu Mar 12 22:07:26 2015 +0100
    10.3 @@ -56,34 +56,41 @@
    10.4  
    10.5    /* resolve inlined files */
    10.6  
    10.7 -  private def find_file(tokens: List[Token]): Option[String] =
    10.8 +  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
    10.9    {
   10.10 -    def clean(toks: List[Token]): List[Token] =
   10.11 +    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
   10.12        toks match {
   10.13 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
   10.14 -        case t :: ts => t :: clean(ts)
   10.15 -        case Nil => Nil
   10.16 +        case (t1, i1) :: (t2, i2) :: rest =>
   10.17 +          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
   10.18 +          else (t1, i1) :: clean((t2, i2) :: rest)
   10.19 +        case _ => toks
   10.20        }
   10.21 -    clean(tokens.filter(_.is_proper)) match {
   10.22 -      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
   10.23 -      case _ => None
   10.24 -    }
   10.25 +    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
   10.26    }
   10.27  
   10.28 -  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
   10.29 +  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
   10.30 +    tokens match {
   10.31 +      case (tok, _) :: toks =>
   10.32 +        if (tok.is_command)
   10.33 +          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
   10.34 +        else None
   10.35 +      case Nil => None
   10.36 +    }
   10.37 +
   10.38 +  def span_files(syntax: Prover.Syntax, span: Span): (List[String], Int) =
   10.39      span.kind match {
   10.40        case Command_Span(name, _) =>
   10.41          syntax.load_command(name) match {
   10.42            case Some(exts) =>
   10.43 -            find_file(span.content) match {
   10.44 -              case Some(file) =>
   10.45 -                if (exts.isEmpty) List(file)
   10.46 -                else exts.map(ext => file + "." + ext)
   10.47 -              case None => Nil
   10.48 +            find_file(clean_tokens(span.content)) match {
   10.49 +              case Some((file, i)) =>
   10.50 +                if (exts.isEmpty) (List(file), i)
   10.51 +                else (exts.map(ext => file + "." + ext), i)
   10.52 +              case None => (Nil, -1)
   10.53              }
   10.54 -          case None => Nil
   10.55 +          case None => (Nil, -1)
   10.56          }
   10.57 -      case _ => Nil
   10.58 +      case _ => (Nil, -1)
   10.59      }
   10.60  
   10.61    def resolve_files(
   10.62 @@ -92,15 +99,17 @@
   10.63        node_name: Document.Node.Name,
   10.64        span: Span,
   10.65        get_blob: Document.Node.Name => Option[Document.Blob])
   10.66 -    : List[Command.Blob] =
   10.67 +    : (List[Command.Blob], Int) =
   10.68    {
   10.69 -    span_files(syntax, span).map(file_name =>
   10.70 -      Exn.capture {
   10.71 -        val name =
   10.72 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   10.73 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   10.74 -        (name, blob)
   10.75 -      })
   10.76 +    val (files, index) = span_files(syntax, span)
   10.77 +    val blobs =
   10.78 +      files.map(file =>
   10.79 +        Exn.capture {
   10.80 +          val name =
   10.81 +            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
   10.82 +          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   10.83 +          (name, blob)
   10.84 +        })
   10.85 +    (blobs, index)
   10.86    }
   10.87  }
   10.88 -
    11.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 12 19:09:18 2015 +0100
    11.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 12 22:07:26 2015 +0100
    11.3 @@ -19,7 +19,7 @@
    11.4    val init_state: state
    11.5    val define_blob: string -> string -> state -> state
    11.6    type blob_digest = (string * string option) Exn.result
    11.7 -  val define_command: Document_ID.command -> string -> blob_digest list ->
    11.8 +  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
    11.9      ((int * int) * string) list -> state -> state
   11.10    val remove_versions: Document_ID.version list -> state -> state
   11.11    val start_execution: state -> state
   11.12 @@ -359,23 +359,37 @@
   11.13    blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
   11.14      (file_node, Option.map (the_blob state) raw_digest));
   11.15  
   11.16 +fun blob_reports pos (blob_digest: blob_digest) =
   11.17 +  (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
   11.18 +
   11.19  
   11.20  (* commands *)
   11.21  
   11.22 -fun define_command command_id name command_blobs toks =
   11.23 +fun define_command command_id name command_blobs blobs_index toks =
   11.24    map_state (fn (versions, blobs, commands, execution) =>
   11.25      let
   11.26        val id = Document_ID.print command_id;
   11.27        val span =
   11.28          Lazy.lazy (fn () =>
   11.29            Position.setmp_thread_data (Position.id_only id)
   11.30 -            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
   11.31 +            (fn () =>
   11.32 +              let
   11.33 +                val (tokens, _) = fold_map Token.make toks (Position.id id);
   11.34 +                val _ =
   11.35 +                  (case try (Token.pos_of o nth tokens) blobs_index of
   11.36 +                    SOME pos =>
   11.37 +                      if Position.is_reported pos then
   11.38 +                        Position.reports
   11.39 +                          ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
   11.40 +                      else ()
   11.41 +                  | NONE => ());
   11.42 +              in tokens end) ());
   11.43 +      val commands' =
   11.44 +        Inttab.update_new (command_id, (name, command_blobs, span)) commands
   11.45 +          handle Inttab.DUP dup => err_dup "command" dup;
   11.46        val _ =
   11.47          Position.setmp_thread_data (Position.id_only id)
   11.48            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
   11.49 -      val commands' =
   11.50 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
   11.51 -          handle Inttab.DUP dup => err_dup "command" dup;
   11.52      in (versions, blobs, commands', execution) end);
   11.53  
   11.54  fun the_command (State {commands, ...}) command_id =
    12.1 --- a/src/Pure/PIDE/protocol.ML	Thu Mar 12 19:09:18 2015 +0100
    12.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Mar 12 22:07:26 2015 +0100
    12.3 @@ -30,17 +30,20 @@
    12.4    Isabelle_Process.protocol_command "Document.define_command"
    12.5      (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
    12.6        let
    12.7 -        val blobs =
    12.8 +        val (blobs, blobs_index) =
    12.9            YXML.parse_body blobs_yxml |>
   12.10              let open XML.Decode in
   12.11 -              list (variant
   12.12 -               [fn ([], a) => Exn.Res (pair string (option string) a),
   12.13 -                fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
   12.14 +              pair
   12.15 +                (list (variant
   12.16 +                 [fn ([], a) => Exn.Res (pair string (option string) a),
   12.17 +                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
   12.18 +                int
   12.19              end;
   12.20          val toks =
   12.21            (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
   12.22        in
   12.23 -        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
   12.24 +        Document.change_state
   12.25 +          (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
   12.26        end);
   12.27  
   12.28  val _ =
    13.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 12 19:09:18 2015 +0100
    13.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 12 22:07:26 2015 +0100
    13.3 @@ -392,7 +392,7 @@
    13.4                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    13.5            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    13.6  
    13.7 -      YXML.string_of_body(list(encode_blob)(command.blobs))
    13.8 +      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    13.9      }
   13.10  
   13.11      val toks = command.span.content
    14.1 --- a/src/Pure/PIDE/resources.scala	Thu Mar 12 19:09:18 2015 +0100
    14.2 +++ b/src/Pure/PIDE/resources.scala	Thu Mar 12 22:07:26 2015 +0100
    14.3 @@ -57,7 +57,7 @@
    14.4    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
    14.5      if (syntax.load_commands_in(text)) {
    14.6        val spans = syntax.parse_spans(text)
    14.7 -      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
    14.8 +      spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList
    14.9      }
   14.10      else Nil
   14.11  
    15.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 19:09:18 2015 +0100
    15.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 22:07:26 2015 +0100
    15.3 @@ -143,8 +143,8 @@
    15.4  
    15.5    @tailrec private def chop_common(
    15.6        cmds: List[Command],
    15.7 -      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
    15.8 -    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
    15.9 +      blobs_spans: List[((List[Command.Blob], Int), Command_Span.Span)])
   15.10 +    : (List[Command], List[((List[Command.Blob], Int), Command_Span.Span)]) =
   15.11    {
   15.12      (cmds, blobs_spans) match {
   15.13        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
   15.14 @@ -179,7 +179,8 @@
   15.15        case cmd :: _ =>
   15.16          val hook = commands.prev(cmd)
   15.17          val inserted =
   15.18 -          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
   15.19 +          blobs_spans2.map({ case (blobs, span) =>
   15.20 +            Command(Document_ID.make(), name, Some(blobs), span) })
   15.21          (commands /: cmds2)(_ - _).append_after(hook, inserted)
   15.22      }
   15.23    }