inline blobs into command, via SHA1 digest;
authorwenzelm
Mon Nov 18 23:26:15 2013 +0100 (2013-11-18)
changeset 545135545aff878b1
parent 54512 7a92ed889da4
child 54514 6428dfab6520
inline blobs into command, via SHA1 digest;
broadcast all blobs within edit, without storing the result;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Nov 18 22:06:08 2013 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Nov 18 23:26:15 2013 +0100
     1.3 @@ -58,11 +58,11 @@
     1.4  
     1.5    def thy_load(span: List[Token]): Option[List[String]] =
     1.6      keywords.get(Command.name(span)) match {
     1.7 -      case Some((Keyword.THY_LOAD, files)) => Some(files)
     1.8 +      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
     1.9        case _ => None
    1.10      }
    1.11  
    1.12 -  def thy_load_commands: List[(String, List[String])] =
    1.13 +  val thy_load_commands: List[(String, List[String])] =
    1.14      (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
    1.15  
    1.16    def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     2.1 --- a/src/Pure/PIDE/command.scala	Mon Nov 18 22:06:08 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Mon Nov 18 23:26:15 2013 +0100
     2.3 @@ -144,11 +144,13 @@
     2.4    def name(span: List[Token]): String =
     2.5      span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
     2.6  
     2.7 +  type Blobs = List[(Document.Node.Name, Option[SHA1.Digest])]
     2.8 +
     2.9    def apply(
    2.10      id: Document_ID.Command,
    2.11      node_name: Document.Node.Name,
    2.12      span: List[Token],
    2.13 -    thy_load: Option[List[String]],
    2.14 +    blobs: Blobs,
    2.15      results: Results = Results.empty,
    2.16      markup: Markup_Tree = Markup_Tree.empty): Command =
    2.17    {
    2.18 @@ -167,14 +169,14 @@
    2.19        i += n
    2.20      }
    2.21  
    2.22 -    new Command(id, node_name, span1.toList, source, thy_load, results, markup)
    2.23 +    new Command(id, node_name, span1.toList, source, blobs, results, markup)
    2.24    }
    2.25  
    2.26 -  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
    2.27 +  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
    2.28  
    2.29    def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
    2.30        : Command =
    2.31 -    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
    2.32 +    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), Nil,
    2.33        results, markup)
    2.34  
    2.35    def unparsed(source: String): Command =
    2.36 @@ -215,7 +217,7 @@
    2.37      val node_name: Document.Node.Name,
    2.38      val span: List[Token],
    2.39      val source: String,
    2.40 -    val thy_load: Option[List[String]],
    2.41 +    val blobs: Command.Blobs,
    2.42      val init_results: Command.Results,
    2.43      val init_markup: Markup_Tree)
    2.44  {
     3.1 --- a/src/Pure/PIDE/document.scala	Mon Nov 18 22:06:08 2013 +0100
     3.2 +++ b/src/Pure/PIDE/document.scala	Mon Nov 18 23:26:15 2013 +0100
     3.3 @@ -154,7 +154,7 @@
     3.4      final class Commands private(val commands: Linear_Set[Command])
     3.5      {
     3.6        lazy val thy_load_commands: List[Command] =
     3.7 -        commands.iterator.filter(_.thy_load.isDefined).toList
     3.8 +        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
     3.9  
    3.10        private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    3.11        {
    3.12 @@ -189,31 +189,27 @@
    3.13      val header: Node.Header = Node.bad_header("Bad theory header"),
    3.14      val perspective: Node.Perspective_Command =
    3.15        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    3.16 -    val blob: Bytes = Bytes.empty,
    3.17      _commands: Node.Commands = Node.Commands.empty)
    3.18    {
    3.19      def clear: Node = new Node(header = header)
    3.20  
    3.21      def update_header(new_header: Node.Header): Node =
    3.22 -      new Node(new_header, perspective, blob, _commands)
    3.23 +      new Node(new_header, perspective, _commands)
    3.24  
    3.25      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    3.26 -      new Node(header, new_perspective, blob, _commands)
    3.27 +      new Node(header, new_perspective, _commands)
    3.28  
    3.29      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    3.30        perspective.required == other_perspective.required &&
    3.31        perspective.visible.same(other_perspective.visible) &&
    3.32        perspective.overlays == other_perspective.overlays
    3.33  
    3.34 -    def update_blob(new_blob: Bytes): Node =
    3.35 -      new Node(header, perspective, new_blob, _commands)
    3.36 -
    3.37      def commands: Linear_Set[Command] = _commands.commands
    3.38      def thy_load_commands: List[Command] = _commands.thy_load_commands
    3.39  
    3.40      def update_commands(new_commands: Linear_Set[Command]): Node =
    3.41        if (new_commands eq _commands.commands) this
    3.42 -      else new Node(header, perspective, blob, Node.Commands(new_commands))
    3.43 +      else new Node(header, perspective, Node.Commands(new_commands))
    3.44  
    3.45      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    3.46        _commands.range(i)
     4.1 --- a/src/Pure/Thy/thy_load.scala	Mon Nov 18 22:06:08 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.scala	Mon Nov 18 23:26:15 2013 +0100
     4.3 @@ -56,39 +56,13 @@
     4.4  
     4.5    /* theory files */
     4.6  
     4.7 -  private def find_file(tokens: List[Token]): Option[String] =
     4.8 -  {
     4.9 -    def clean(toks: List[Token]): List[Token] =
    4.10 -      toks match {
    4.11 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    4.12 -        case t :: ts => t :: clean(ts)
    4.13 -        case Nil => Nil
    4.14 -      }
    4.15 -    val clean_tokens = clean(tokens.filter(_.is_proper))
    4.16 -    clean_tokens.reverse.find(_.is_name).map(_.content)
    4.17 -  }
    4.18 -
    4.19    def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
    4.20      syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    4.21  
    4.22    def body_files(syntax: Outer_Syntax, text: String): List[String] =
    4.23    {
    4.24 -    val thy_load_commands = syntax.thy_load_commands
    4.25      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    4.26 -    spans.iterator.map({
    4.27 -      case toks @ (tok :: _) if tok.is_command =>
    4.28 -        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
    4.29 -          case Some((_, exts)) =>
    4.30 -            find_file(toks) match {
    4.31 -              case Some(file) =>
    4.32 -                if (exts.isEmpty) List(file)
    4.33 -                else exts.map(ext => file + "." + ext)
    4.34 -              case None => Nil
    4.35 -            }
    4.36 -          case None => Nil
    4.37 -        }
    4.38 -      case _ => Nil
    4.39 -    }).flatten.toList
    4.40 +    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
    4.41    }
    4.42  
    4.43    def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 22:06:08 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 23:26:15 2013 +0100
     5.3 @@ -68,7 +68,7 @@
     5.4        /* result structure */
     5.5  
     5.6        val spans = parse_spans(syntax.scan(text))
     5.7 -      spans.foreach(span => add(Command(Document_ID.none, node_name, span, syntax.thy_load(span))))
     5.8 +      spans.foreach(span => add(Command(Document_ID.none, node_name, span, Nil)))
     5.9        result()
    5.10      }
    5.11    }
    5.12 @@ -225,23 +225,69 @@
    5.13    }
    5.14  
    5.15  
    5.16 +  /* inlined files */
    5.17 +
    5.18 +  private def find_file(tokens: List[Token]): Option[String] =
    5.19 +  {
    5.20 +    def clean(toks: List[Token]): List[Token] =
    5.21 +      toks match {
    5.22 +        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
    5.23 +        case t :: ts => t :: clean(ts)
    5.24 +        case Nil => Nil
    5.25 +      }
    5.26 +    val clean_tokens = clean(tokens.filter(_.is_proper))
    5.27 +    clean_tokens.reverse.find(_.is_name).map(_.content)
    5.28 +  }
    5.29 +
    5.30 +  def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
    5.31 +    syntax.thy_load(span) match {
    5.32 +      case Some(exts) =>
    5.33 +        find_file(span) match {
    5.34 +          case Some(file) =>
    5.35 +            if (exts.isEmpty) List(file)
    5.36 +            else exts.map(ext => file + "." + ext)
    5.37 +          case None => Nil
    5.38 +        }
    5.39 +      case None => Nil
    5.40 +    }
    5.41 +
    5.42 +  def resolve_files(
    5.43 +      syntax: Outer_Syntax,
    5.44 +      all_blobs: Map[Document.Node.Name, Bytes],
    5.45 +      name: Document.Node.Name,
    5.46 +      span: List[Token]): Command.Blobs =
    5.47 +  {
    5.48 +    val files = span_files(syntax, span)
    5.49 +    files.map(file => {
    5.50 +      // FIXME proper thy_load append
    5.51 +      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
    5.52 +      (file_name, all_blobs.get(file_name).map(_.sha1_digest))
    5.53 +    })
    5.54 +  }
    5.55 +
    5.56 +
    5.57    /* reparse range of command spans */
    5.58  
    5.59    @tailrec private def chop_common(
    5.60 -      cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
    5.61 +      cmds: List[Command], spans: List[(List[Token], Command.Blobs)])
    5.62 +      : (List[Command], List[(List[Token], Command.Blobs)]) =
    5.63      (cmds, spans) match {
    5.64 -      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
    5.65 +      case (c :: cs, (span, blobs) :: ps) if c.span == span && c.blobs == blobs =>
    5.66 +        chop_common(cs, ps)
    5.67        case _ => (cmds, spans)
    5.68      }
    5.69  
    5.70    private def reparse_spans(
    5.71      syntax: Outer_Syntax,
    5.72 +    all_blobs: Map[Document.Node.Name, Bytes],
    5.73      name: Document.Node.Name,
    5.74      commands: Linear_Set[Command],
    5.75      first: Command, last: Command): Linear_Set[Command] =
    5.76    {
    5.77      val cmds0 = commands.iterator(first, last).toList
    5.78 -    val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
    5.79 +    val spans0 =
    5.80 +      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    5.81 +        map(span => (span, resolve_files(syntax, all_blobs, name, span)))
    5.82  
    5.83      val (cmds1, spans1) = chop_common(cmds0, spans0)
    5.84  
    5.85 @@ -256,7 +302,7 @@
    5.86        case cmd :: _ =>
    5.87          val hook = commands.prev(cmd)
    5.88          val inserted =
    5.89 -          spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span)))
    5.90 +          spans2.map({ case (span, blobs) => Command(Document_ID.make(), name, span, blobs) })
    5.91          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    5.92      }
    5.93    }
    5.94 @@ -267,6 +313,7 @@
    5.95    // FIXME somewhat slow
    5.96    private def recover_spans(
    5.97      syntax: Outer_Syntax,
    5.98 +    all_blobs: Map[Document.Node.Name, Bytes],
    5.99      name: Document.Node.Name,
   5.100      perspective: Command.Perspective,
   5.101      commands: Linear_Set[Command]): Linear_Set[Command] =
   5.102 @@ -282,7 +329,7 @@
   5.103          case Some(first_unparsed) =>
   5.104            val first = next_invisible_command(cmds.reverse, first_unparsed)
   5.105            val last = next_invisible_command(cmds, first_unparsed)
   5.106 -          recover(reparse_spans(syntax, name, cmds, first, last))
   5.107 +          recover(reparse_spans(syntax, all_blobs, name, cmds, first, last))
   5.108          case None => cmds
   5.109        }
   5.110      recover(commands)
   5.111 @@ -293,6 +340,7 @@
   5.112  
   5.113    private def consolidate_spans(
   5.114      syntax: Outer_Syntax,
   5.115 +    all_blobs: Map[Document.Node.Name, Bytes],
   5.116      reparse_limit: Int,
   5.117      name: Document.Node.Name,
   5.118      perspective: Command.Perspective,
   5.119 @@ -312,7 +360,7 @@
   5.120                  last = it.next
   5.121                  i += last.length
   5.122                }
   5.123 -              reparse_spans(syntax, name, commands, first_unfinished, last)
   5.124 +              reparse_spans(syntax, all_blobs, name, commands, first_unfinished, last)
   5.125              case None => commands
   5.126            }
   5.127          case None => commands
   5.128 @@ -333,7 +381,10 @@
   5.129      inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   5.130    }
   5.131  
   5.132 -  private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
   5.133 +  private def text_edit(
   5.134 +    syntax: Outer_Syntax,
   5.135 +    all_blobs: Map[Document.Node.Name, Bytes],
   5.136 +    reparse_limit: Int,
   5.137      node: Document.Node, edit: Document.Edit_Text): Document.Node =
   5.138    {
   5.139      edit match {
   5.140 @@ -342,7 +393,7 @@
   5.141        case (name, Document.Node.Edits(text_edits)) =>
   5.142          val commands0 = node.commands
   5.143          val commands1 = edit_text(text_edits, commands0)
   5.144 -        val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
   5.145 +        val commands2 = recover_spans(syntax, all_blobs, name, node.perspective.visible, commands1)
   5.146          node.update_commands(commands2)
   5.147  
   5.148        case (_, Document.Node.Deps(_)) => node
   5.149 @@ -354,9 +405,9 @@
   5.150          if (node.same_perspective(perspective)) node
   5.151          else
   5.152            node.update_perspective(perspective).update_commands(
   5.153 -            consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
   5.154 +            consolidate_spans(syntax, all_blobs, reparse_limit, name, visible, node.commands))
   5.155  
   5.156 -      case (_, Document.Node.Blob(blob)) => node.update_blob(blob)
   5.157 +      case (_, Document.Node.Blob(_)) => node
   5.158      }
   5.159    }
   5.160  
   5.161 @@ -377,6 +428,14 @@
   5.162        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   5.163          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   5.164  
   5.165 +    val all_blobs: Map[Document.Node.Name, Bytes] =
   5.166 +      (Map.empty[Document.Node.Name, Bytes] /: node_edits) {
   5.167 +        case (bs1, (_, es)) => (bs1 /: es) {
   5.168 +          case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob)
   5.169 +          case (bs, _) => bs
   5.170 +        }
   5.171 +      }
   5.172 +
   5.173      node_edits foreach {
   5.174        case (name, edits) =>
   5.175          val node = nodes(name)
   5.176 @@ -384,9 +443,10 @@
   5.177  
   5.178          val node1 =
   5.179            if (reparse_set(name) && !commands.isEmpty)
   5.180 -            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
   5.181 +            node.update_commands(
   5.182 +              reparse_spans(syntax, all_blobs, name, commands, commands.head, commands.last))
   5.183            else node
   5.184 -        val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
   5.185 +        val node2 = (node1 /: edits)(text_edit(syntax, all_blobs, reparse_limit, _, _))
   5.186  
   5.187          if (!(node.same_perspective(node2.perspective)))
   5.188            doc_edits += (name -> node2.perspective)
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 22:06:08 2013 +0100
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 23:26:15 2013 +0100
     6.3 @@ -190,7 +190,7 @@
     6.4        val clear = pending_clear
     6.5        val edits = snapshot()
     6.6        val perspective = node_perspective()
     6.7 -      if (clear || !edits.isEmpty || last_perspective != perspective) {
     6.8 +      if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) {
     6.9          pending_clear = false
    6.10          pending.clear
    6.11          last_perspective = perspective