tuned signature;
authorwenzelm
Sat Jan 07 19:36:40 2017 +0100 (2017-01-07 ago)
changeset 6482378df3d65a1cc
parent 64822 c8bac4b0ef07
child 64824 330ec9bc4b75
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Jan 07 17:32:11 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Jan 07 19:36:40 2017 +0100
     1.3 @@ -351,8 +351,8 @@
     1.4        // inlined errors
     1.5        case Thy_Header.THEORY =>
     1.6          val header =
     1.7 -          resources.check_thy_reader("", node_name,
     1.8 -            new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
     1.9 +          resources.check_thy_reader(
    1.10 +            "", node_name, new CharSequenceReader(Token.implode(span.content)))
    1.11          val errors =
    1.12            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    1.13              val msg =
     2.1 --- a/src/Pure/PIDE/resources.scala	Sat Jan 07 17:32:11 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 19:36:40 2017 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4    }
     2.5  
     2.6    def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
     2.7 -    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
     2.8 +    reader: Reader[Char], start: Token.Pos = Token.Pos.command): Document.Node.Header =
     2.9    {
    2.10      if (reader.source.length > 0) {
    2.11        try {
    2.12 @@ -140,7 +140,7 @@
    2.13      else Document.Node.no_header
    2.14    }
    2.15  
    2.16 -  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
    2.17 +  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
    2.18      : Document.Node.Header =
    2.19      with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
    2.20  
     3.1 --- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 17:32:11 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
     3.3 @@ -47,8 +47,7 @@
     3.4      resources.special_header(node_name) getOrElse
     3.5      {
     3.6        if (is_theory)
     3.7 -        resources.check_thy_reader(
     3.8 -          "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
     3.9 +        resources.check_thy_reader("", node_name, new CharSequenceReader(doc.text))
    3.10        else Document.Node.no_header
    3.11      }
    3.12  
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 17:32:11 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
     4.3 @@ -242,8 +242,7 @@
     4.4      PIDE.resources.special_header(node_name) getOrElse
     4.5      {
     4.6        if (is_theory)
     4.7 -        PIDE.resources.check_thy_reader(
     4.8 -          "", node_name, new CharSequenceReader(content.text), Token.Pos.command)
     4.9 +        PIDE.resources.check_thy_reader("", node_name, new CharSequenceReader(content.text))
    4.10        else Document.Node.no_header
    4.11      }
    4.12  
    4.13 @@ -320,7 +319,7 @@
    4.14                case Some(offset) =>
    4.15                  val length = buffer.getLength - offset
    4.16                  PIDE.resources.check_thy_reader("", node_name,
    4.17 -                  new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
    4.18 +                  new CharSequenceReader(buffer.getSegment(offset, length)))
    4.19                case None =>
    4.20                  Document.Node.no_header
    4.21              }