proper Thy_Load.append of auxiliary file names;
authorwenzelm
Tue Nov 19 13:39:12 2013 +0100 (2013-11-19)
changeset 54517044bee8c5e69
parent 54516 2a7f9e79cb28
child 54518 81a9a54c57fc
proper Thy_Load.append of auxiliary file names;
inlined errors;
src/Pure/PIDE/command.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/jedit_thy_load.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Nov 19 13:13:51 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Nov 19 13:39:12 2013 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4    def name(span: List[Token]): String =
     1.5      span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
     1.6  
     1.7 -  type Blobs = List[(Document.Node.Name, Option[SHA1.Digest])]
     1.8 +  type Blobs = List[Exn.Result[(Document.Node.Name, SHA1.Digest)]]
     1.9  
    1.10    def apply(
    1.11      id: Document_ID.Command,
     2.1 --- a/src/Pure/Thy/thy_load.scala	Tue Nov 19 13:13:51 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Nov 19 13:39:12 2013 +0100
     2.3 @@ -101,6 +101,6 @@
     2.4  
     2.5    def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
     2.6        : (List[Document.Edit_Command], Document.Version) =
     2.7 -    Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
     2.8 +    Thy_Syntax.text_edits(this, reparse_limit, previous, edits)
     2.9  }
    2.10  
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:13:51 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:39:12 2013 +0100
     3.3 @@ -252,17 +252,23 @@
     3.4      }
     3.5  
     3.6    def resolve_files(
     3.7 +      thy_load: Thy_Load,
     3.8        syntax: Outer_Syntax,
     3.9 -      all_blobs: Map[Document.Node.Name, Bytes],
    3.10 -      name: Document.Node.Name,
    3.11 -      span: List[Token]): Command.Blobs =
    3.12 +      node_name: Document.Node.Name,
    3.13 +      span: List[Token],
    3.14 +      all_blobs: Map[Document.Node.Name, Bytes])
    3.15 +    : Command.Blobs =
    3.16    {
    3.17 -    val files = span_files(syntax, span)
    3.18 -    files.map(file => {
    3.19 -      // FIXME proper thy_load append
    3.20 -      val file_name = Document.Node.Name(name.master_dir + file)
    3.21 -      (file_name, all_blobs.get(file_name).map(_.sha1_digest))
    3.22 -    })
    3.23 +    span_files(syntax, span).map(file =>
    3.24 +      Exn.capture {
    3.25 +        val name =
    3.26 +          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
    3.27 +        all_blobs.get(name) match {
    3.28 +          case Some(blob) => (name, blob.sha1_digest)
    3.29 +          case None => error("Bad file: " + quote(name.toString))
    3.30 +        }
    3.31 +      }
    3.32 +    )
    3.33    }
    3.34  
    3.35  
    3.36 @@ -278,6 +284,7 @@
    3.37      }
    3.38  
    3.39    private def reparse_spans(
    3.40 +    thy_load: Thy_Load,
    3.41      syntax: Outer_Syntax,
    3.42      all_blobs: Map[Document.Node.Name, Bytes],
    3.43      name: Document.Node.Name,
    3.44 @@ -287,7 +294,7 @@
    3.45      val cmds0 = commands.iterator(first, last).toList
    3.46      val spans0 =
    3.47        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
    3.48 -        map(span => (span, resolve_files(syntax, all_blobs, name, span)))
    3.49 +        map(span => (span, resolve_files(thy_load, syntax, name, span, all_blobs)))
    3.50  
    3.51      val (cmds1, spans1) = chop_common(cmds0, spans0)
    3.52  
    3.53 @@ -312,6 +319,7 @@
    3.54  
    3.55    // FIXME somewhat slow
    3.56    private def recover_spans(
    3.57 +    thy_load: Thy_Load,
    3.58      syntax: Outer_Syntax,
    3.59      all_blobs: Map[Document.Node.Name, Bytes],
    3.60      name: Document.Node.Name,
    3.61 @@ -329,7 +337,7 @@
    3.62          case Some(first_unparsed) =>
    3.63            val first = next_invisible_command(cmds.reverse, first_unparsed)
    3.64            val last = next_invisible_command(cmds, first_unparsed)
    3.65 -          recover(reparse_spans(syntax, all_blobs, name, cmds, first, last))
    3.66 +          recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last))
    3.67          case None => cmds
    3.68        }
    3.69      recover(commands)
    3.70 @@ -339,6 +347,7 @@
    3.71    /* consolidate unfinished spans */
    3.72  
    3.73    private def consolidate_spans(
    3.74 +    thy_load: Thy_Load,
    3.75      syntax: Outer_Syntax,
    3.76      all_blobs: Map[Document.Node.Name, Bytes],
    3.77      reparse_limit: Int,
    3.78 @@ -360,7 +369,7 @@
    3.79                  last = it.next
    3.80                  i += last.length
    3.81                }
    3.82 -              reparse_spans(syntax, all_blobs, name, commands, first_unfinished, last)
    3.83 +              reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last)
    3.84              case None => commands
    3.85            }
    3.86          case None => commands
    3.87 @@ -382,6 +391,7 @@
    3.88    }
    3.89  
    3.90    private def text_edit(
    3.91 +    thy_load: Thy_Load,
    3.92      syntax: Outer_Syntax,
    3.93      all_blobs: Map[Document.Node.Name, Bytes],
    3.94      reparse_limit: Int,
    3.95 @@ -393,7 +403,8 @@
    3.96        case (name, Document.Node.Edits(text_edits)) =>
    3.97          val commands0 = node.commands
    3.98          val commands1 = edit_text(text_edits, commands0)
    3.99 -        val commands2 = recover_spans(syntax, all_blobs, name, node.perspective.visible, commands1)
   3.100 +        val commands2 =
   3.101 +          recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1)
   3.102          node.update_commands(commands2)
   3.103  
   3.104        case (_, Document.Node.Deps(_)) => node
   3.105 @@ -405,20 +416,22 @@
   3.106          if (node.same_perspective(perspective)) node
   3.107          else
   3.108            node.update_perspective(perspective).update_commands(
   3.109 -            consolidate_spans(syntax, all_blobs, reparse_limit, name, visible, node.commands))
   3.110 +            consolidate_spans(thy_load, syntax, all_blobs, reparse_limit,
   3.111 +              name, visible, node.commands))
   3.112  
   3.113        case (_, Document.Node.Blob(_)) => node
   3.114      }
   3.115    }
   3.116  
   3.117    def text_edits(
   3.118 -      base_syntax: Outer_Syntax,
   3.119 +      thy_load: Thy_Load,
   3.120        reparse_limit: Int,
   3.121        previous: Document.Version,
   3.122        edits: List[Document.Edit_Text])
   3.123      : (List[Document.Edit_Command], Document.Version) =
   3.124    {
   3.125 -    val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits)
   3.126 +    val (syntax, reparse, nodes0, doc_edits0) =
   3.127 +      header_edits(thy_load.base_syntax, previous, edits)
   3.128      val reparse_set = reparse.toSet
   3.129  
   3.130      var nodes = nodes0
   3.131 @@ -444,9 +457,10 @@
   3.132          val node1 =
   3.133            if (reparse_set(name) && !commands.isEmpty)
   3.134              node.update_commands(
   3.135 -              reparse_spans(syntax, all_blobs, name, commands, commands.head, commands.last))
   3.136 +              reparse_spans(thy_load, syntax, all_blobs,
   3.137 +                name, commands, commands.head, commands.last))
   3.138            else node
   3.139 -        val node2 = (node1 /: edits)(text_edit(syntax, all_blobs, reparse_limit, _, _))
   3.140 +        val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _))
   3.141  
   3.142          if (!(node.same_perspective(node2.perspective)))
   3.143            doc_edits += (name -> node2.perspective)
     4.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Nov 19 13:13:51 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Nov 19 13:39:12 2013 +0100
     4.3 @@ -42,7 +42,7 @@
     4.4    override def append(dir: String, source_path: Path): String =
     4.5    {
     4.6      val path = source_path.expand
     4.7 -    if (path.is_absolute) Isabelle_System.platform_path(path)
     4.8 +    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
     4.9      else {
    4.10        val vfs = VFSManager.getVFSForPath(dir)
    4.11        if (vfs.isInstanceOf[FileVFS])