src/Pure/Thy/thy_syntax.scala
changeset 54517 044bee8c5e69
parent 54515 570ba266f5b5
child 54518 81a9a54c57fc
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:13:51 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:39:12 2013 +0100
     1.3 @@ -252,17 +252,23 @@
     1.4      }
     1.5  
     1.6    def resolve_files(
     1.7 +      thy_load: Thy_Load,
     1.8        syntax: Outer_Syntax,
     1.9 -      all_blobs: Map[Document.Node.Name, Bytes],
    1.10 -      name: Document.Node.Name,
    1.11 -      span: List[Token]): Command.Blobs =
    1.12 +      node_name: Document.Node.Name,
    1.13 +      span: List[Token],
    1.14 +      all_blobs: Map[Document.Node.Name, Bytes])
    1.15 +    : Command.Blobs =
    1.16    {
    1.17 -    val files = span_files(syntax, span)
    1.18 -    files.map(file => {
    1.19 -      // FIXME proper thy_load append
    1.20 -      val file_name = Document.Node.Name(name.master_dir + file)
    1.21 -      (file_name, all_blobs.get(file_name).map(_.sha1_digest))
    1.22 -    })
    1.23 +    span_files(syntax, span).map(file =>
    1.24 +      Exn.capture {
    1.25 +        val name =
    1.26 +          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
    1.27 +        all_blobs.get(name) match {
    1.28 +          case Some(blob) => (name, blob.sha1_digest)
    1.29 +          case None => error("Bad file: " + quote(name.toString))
    1.30 +        }
    1.31 +      }
    1.32 +    )
    1.33    }
    1.34  
    1.35  
    1.36 @@ -278,6 +284,7 @@
    1.37      }
    1.38  
    1.39    private def reparse_spans(
    1.40 +    thy_load: Thy_Load,
    1.41      syntax: Outer_Syntax,
    1.42      all_blobs: Map[Document.Node.Name, Bytes],
    1.43      name: Document.Node.Name,
    1.44 @@ -287,7 +294,7 @@
    1.45      val cmds0 = commands.iterator(first, last).toList
    1.46      val spans0 =
    1.47        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    1.48 -        map(span => (span, resolve_files(syntax, all_blobs, name, span)))
    1.49 +        map(span => (span, resolve_files(thy_load, syntax, name, span, all_blobs)))
    1.50  
    1.51      val (cmds1, spans1) = chop_common(cmds0, spans0)
    1.52  
    1.53 @@ -312,6 +319,7 @@
    1.54  
    1.55    // FIXME somewhat slow
    1.56    private def recover_spans(
    1.57 +    thy_load: Thy_Load,
    1.58      syntax: Outer_Syntax,
    1.59      all_blobs: Map[Document.Node.Name, Bytes],
    1.60      name: Document.Node.Name,
    1.61 @@ -329,7 +337,7 @@
    1.62          case Some(first_unparsed) =>
    1.63            val first = next_invisible_command(cmds.reverse, first_unparsed)
    1.64            val last = next_invisible_command(cmds, first_unparsed)
    1.65 -          recover(reparse_spans(syntax, all_blobs, name, cmds, first, last))
    1.66 +          recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last))
    1.67          case None => cmds
    1.68        }
    1.69      recover(commands)
    1.70 @@ -339,6 +347,7 @@
    1.71    /* consolidate unfinished spans */
    1.72  
    1.73    private def consolidate_spans(
    1.74 +    thy_load: Thy_Load,
    1.75      syntax: Outer_Syntax,
    1.76      all_blobs: Map[Document.Node.Name, Bytes],
    1.77      reparse_limit: Int,
    1.78 @@ -360,7 +369,7 @@
    1.79                  last = it.next
    1.80                  i += last.length
    1.81                }
    1.82 -              reparse_spans(syntax, all_blobs, name, commands, first_unfinished, last)
    1.83 +              reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last)
    1.84              case None => commands
    1.85            }
    1.86          case None => commands
    1.87 @@ -382,6 +391,7 @@
    1.88    }
    1.89  
    1.90    private def text_edit(
    1.91 +    thy_load: Thy_Load,
    1.92      syntax: Outer_Syntax,
    1.93      all_blobs: Map[Document.Node.Name, Bytes],
    1.94      reparse_limit: Int,
    1.95 @@ -393,7 +403,8 @@
    1.96        case (name, Document.Node.Edits(text_edits)) =>
    1.97          val commands0 = node.commands
    1.98          val commands1 = edit_text(text_edits, commands0)
    1.99 -        val commands2 = recover_spans(syntax, all_blobs, name, node.perspective.visible, commands1)
   1.100 +        val commands2 =
   1.101 +          recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1)
   1.102          node.update_commands(commands2)
   1.103  
   1.104        case (_, Document.Node.Deps(_)) => node
   1.105 @@ -405,20 +416,22 @@
   1.106          if (node.same_perspective(perspective)) node
   1.107          else
   1.108            node.update_perspective(perspective).update_commands(
   1.109 -            consolidate_spans(syntax, all_blobs, reparse_limit, name, visible, node.commands))
   1.110 +            consolidate_spans(thy_load, syntax, all_blobs, reparse_limit,
   1.111 +              name, visible, node.commands))
   1.112  
   1.113        case (_, Document.Node.Blob(_)) => node
   1.114      }
   1.115    }
   1.116  
   1.117    def text_edits(
   1.118 -      base_syntax: Outer_Syntax,
   1.119 +      thy_load: Thy_Load,
   1.120        reparse_limit: Int,
   1.121        previous: Document.Version,
   1.122        edits: List[Document.Edit_Text])
   1.123      : (List[Document.Edit_Command], Document.Version) =
   1.124    {
   1.125 -    val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits)
   1.126 +    val (syntax, reparse, nodes0, doc_edits0) =
   1.127 +      header_edits(thy_load.base_syntax, previous, edits)
   1.128      val reparse_set = reparse.toSet
   1.129  
   1.130      var nodes = nodes0
   1.131 @@ -444,9 +457,10 @@
   1.132          val node1 =
   1.133            if (reparse_set(name) && !commands.isEmpty)
   1.134              node.update_commands(
   1.135 -              reparse_spans(syntax, all_blobs, name, commands, commands.head, commands.last))
   1.136 +              reparse_spans(thy_load, syntax, all_blobs,
   1.137 +                name, commands, commands.head, commands.last))
   1.138            else node
   1.139 -        val node2 = (node1 /: edits)(text_edit(syntax, all_blobs, reparse_limit, _, _))
   1.140 +        val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _))
   1.141  
   1.142          if (!(node.same_perspective(node2.perspective)))
   1.143            doc_edits += (name -> node2.perspective)