src/Pure/PIDE/resources.scala
changeset 64825 e78b62c289bb
parent 64823 78df3d65a1cc
child 64826 c97296294f6d
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Jan 07 20:01:05 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 20:37:48 2017 +0100
     1.3 @@ -118,11 +118,12 @@
     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 = Token.Pos.command): Document.Node.Header =
     1.8 +      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
     1.9 +    : Document.Node.Header =
    1.10    {
    1.11      if (reader.source.length > 0) {
    1.12        try {
    1.13 -        val header = Thy_Header.read(reader, start).decode_symbols
    1.14 +        val header = Thy_Header.read(reader, start, strict).decode_symbols
    1.15  
    1.16          val base_name = Long_Name.base_name(node_name.theory)
    1.17          val (name, pos) = header.name
    1.18 @@ -140,9 +141,9 @@
    1.19      else Document.Node.no_header
    1.20    }
    1.21  
    1.22 -  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
    1.23 -    : Document.Node.Header =
    1.24 -    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
    1.25 +  def check_thy(qualifier: String, name: Document.Node.Name,
    1.26 +      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
    1.27 +    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
    1.28  
    1.29    def check_file(file: String): Boolean =
    1.30      try {