uniform system name;
authorwenzelm
Wed Oct 25 11:35:48 2017 +0200 (20 months ago)
changeset 66914fb3f13a9c756
parent 66913 7cdd4d59e95c
child 66915 f4259adc928a
uniform system name;
src/Pure/Isar/parse.scala
src/Pure/Isar/token.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Isar/parse.scala	Tue Oct 24 21:20:55 2017 +0200
     1.2 +++ b/src/Pure/Isar/parse.scala	Wed Oct 25 11:35:48 2017 +0200
     1.3 @@ -72,8 +72,8 @@
     1.4      def path: Parser[String] =
     1.5        atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
     1.6  
     1.7 -    def theory_name: Parser[String] =
     1.8 -      atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
     1.9 +    def session_name: Parser[String] = atom("session name", _.is_system_name)
    1.10 +    def theory_name: Parser[String] = atom("theory name", _.is_system_name)
    1.11  
    1.12      private def tag_name: Parser[String] =
    1.13        atom("tag name", tok =>
     2.1 --- a/src/Pure/Isar/token.scala	Tue Oct 24 21:20:55 2017 +0200
     2.2 +++ b/src/Pure/Isar/token.scala	Wed Oct 25 11:35:48 2017 +0200
     2.3 @@ -305,4 +305,6 @@
     2.4      else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
     2.5      else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source)
     2.6      else source
     2.7 +
     2.8 +  def is_system_name: Boolean = is_name && Path.is_wellformed(content)
     2.9  }
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 24 21:20:55 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Wed Oct 25 11:35:48 2017 +0200
     3.3 @@ -582,8 +582,6 @@
     3.4  
     3.5      private val session_entry: Parser[Session_Entry] =
     3.6      {
     3.7 -      val session_name = atom("session name", _.is_name)
     3.8 -
     3.9        val option =
    3.10          option_name ~ opt($$$("=") ~! option_value ^^
    3.11            { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }