tuned signature;
authorwenzelm
Sat Aug 13 16:04:28 2011 +0200 (2011-08-13)
changeset 441831de22a7b2a82
parent 44182 ecb51b457064
child 44184 49501dc1a7b8
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 13 16:04:28 2011 +0200
     1.3 @@ -53,9 +53,9 @@
     1.4      case class Edits[A](edits: List[A]) extends Edit[A]
     1.5      case class Header[A](header: Node_Header) extends Edit[A]
     1.6  
     1.7 -    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
     1.8 +    def norm_header[A](f: String => String, header: Node_Header): Header[A] =
     1.9        header match {
    1.10 -        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
    1.11 +        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(f) })
    1.12          case exn => Header[A](exn)
    1.13        }
    1.14  
     2.1 --- a/src/Pure/System/session.scala	Sat Aug 13 15:59:26 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 13 16:04:28 2011 +0200
     2.3 @@ -189,7 +189,8 @@
     2.4        val syntax = current_syntax()
     2.5        val previous = global_state().history.tip.version
     2.6        val norm_header =
     2.7 -        Document.Node.norm_header[Text.Edit](file_store.append(master_dir, _), header)
     2.8 +        Document.Node.norm_header[Text.Edit](
     2.9 +          name => file_store.append(master_dir, Path.explode(name)), header)
    2.10        val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    2.11        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    2.12        val change =