misc tuning -- more uniform ML vs. Scala;
authorwenzelm
Sat Mar 14 18:18:40 2015 +0100 (2015-03-14)
changeset 59694d2bb4b5ed862
parent 59693 d96cb03caf9e
child 59695 a03e0561bdbf
misc tuning -- more uniform ML vs. Scala;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 14 17:23:58 2015 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 14 18:18:40 2015 +0100
     1.3 @@ -86,20 +86,21 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
     1.8 +  def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char])
     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).decode_symbols
    1.14  
    1.15 -        val base_name = Long_Name.base_name(name.theory)
    1.16 -        val name1 = header.name
    1.17 -        if (base_name != name1)
    1.18 +        val base_name = Long_Name.base_name(node_name.theory)
    1.19 +        val (name, pos) = header.name
    1.20 +        if (base_name != name)
    1.21            error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
    1.22 -            " for theory " + quote(name1))
    1.23 +            " for theory " + quote(name) + Position.here(pos))
    1.24  
    1.25 -        val imports = header.imports.map(import_name(qualifier, name, _))
    1.26 +        val imports =
    1.27 +          header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) })
    1.28          Document.Node.Header(imports, header.keywords, Nil)
    1.29        }
    1.30        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     2.1 --- a/src/Pure/Thy/thy_header.ML	Sat Mar 14 17:23:58 2015 +0100
     2.2 +++ b/src/Pure/Thy/thy_header.ML	Sat Mar 14 18:18:40 2015 +0100
     2.3 @@ -103,8 +103,9 @@
     2.4  
     2.5  local
     2.6  
     2.7 -val imports =
     2.8 -  Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
     2.9 +fun imports name =
    2.10 +  if name = Context.PureN then Scan.succeed []
    2.11 +  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
    2.12  
    2.13  val opt_files =
    2.14    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
    2.15 @@ -128,7 +129,7 @@
    2.16  
    2.17  val args =
    2.18    Parse.position Parse.theory_name :|-- (fn (name, pos) =>
    2.19 -    (if name = Context.PureN then Scan.succeed [] else imports) --
    2.20 +    imports name --
    2.21      Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
    2.22      Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
    2.23  
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sat Mar 14 17:23:58 2015 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Mar 14 18:18:40 2015 +0100
     3.3 @@ -80,11 +80,10 @@
     3.4  
     3.5    val header: Parser[Thy_Header] =
     3.6    {
     3.7 -    val file_name = atom("file name", _.is_name)
     3.8 -
     3.9      val opt_files =
    3.10        $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
    3.11        success(Nil)
    3.12 +
    3.13      val keyword_spec =
    3.14        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    3.15        { case x ~ y ~ z => ((x, y), z) }
    3.16 @@ -94,17 +93,14 @@
    3.17        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    3.18        opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    3.19        { case xs ~ y ~ z => xs.map((_, y, z)) }
    3.20 +
    3.21      val keyword_decls =
    3.22        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    3.23        { case xs ~ yss => (xs :: yss).flatten }
    3.24  
    3.25 -    val file =
    3.26 -      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    3.27 -      file_name ^^ (x => (x, true))
    3.28 -
    3.29      val args =
    3.30 -      theory_name ~
    3.31 -      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
    3.32 +      position(theory_name) ~
    3.33 +      (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
    3.34          { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.35        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
    3.36          { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.37 @@ -156,19 +152,15 @@
    3.38  
    3.39  
    3.40  sealed case class Thy_Header(
    3.41 -  name: String,
    3.42 -  imports: List[String],
    3.43 +  name: (String, Position.T),
    3.44 +  imports: List[(String, Position.T)],
    3.45    keywords: Thy_Header.Keywords)
    3.46  {
    3.47 -  def map(f: String => String): Thy_Header =
    3.48 -    Thy_Header(f(name), imports.map(f), keywords)
    3.49 -
    3.50    def decode_symbols: Thy_Header =
    3.51    {
    3.52      val f = Symbol.decode _
    3.53 -    Thy_Header(f(name), imports.map(f),
    3.54 +    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
    3.55        keywords.map({ case (a, b, c) =>
    3.56          (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
    3.57    }
    3.58  }
    3.59 -