src/Pure/PIDE/resources.scala
changeset 64823 78df3d65a1cc
parent 64797 891a25a87ea1
child 64825 e78b62c289bb
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Jan 07 17:32:11 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 19:36:40 2017 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4    }
     1.5  
     1.6    def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
     1.7 -    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
     1.8 +    reader: Reader[Char], start: Token.Pos = Token.Pos.command): Document.Node.Header =
     1.9    {
    1.10      if (reader.source.length > 0) {
    1.11        try {
    1.12 @@ -140,7 +140,7 @@
    1.13      else Document.Node.no_header
    1.14    }
    1.15  
    1.16 -  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
    1.17 +  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
    1.18      : Document.Node.Header =
    1.19      with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
    1.20