clarified path checks: avoid crash of rendering due to spurious errors;
authorwenzelm
Mon Mar 03 11:58:07 2014 +0100 (2014-03-03 ago)
changeset 55879ac979f750c1a
parent 55878 6d092a5166f1
child 55880 12f9a54ac64f
clarified path checks: avoid crash of rendering due to spurious errors;
src/Pure/General/path.scala
src/Pure/Isar/parse.scala
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/path.scala	Mon Mar 03 11:37:06 2014 +0100
     1.2 +++ b/src/Pure/General/path.scala	Mon Mar 03 11:58:07 2014 +0100
     1.3 @@ -97,9 +97,12 @@
     1.4      new Path(norm_elems(elems.reverse ::: roots))
     1.5    }
     1.6  
     1.7 -  def is_ok(str: String): Boolean =
     1.8 +  def is_wellformed(str: String): Boolean =
     1.9      try { explode(str); true } catch { case ERROR(_) => false }
    1.10  
    1.11 +  def is_valid(str: String): Boolean =
    1.12 +    try { explode(str).expand; true } catch { case ERROR(_) => false }
    1.13 +
    1.14    def split(str: String): List[Path] =
    1.15      space_explode(':', str).filterNot(_.isEmpty).map(explode)
    1.16  
     2.1 --- a/src/Pure/Isar/parse.scala	Mon Mar 03 11:37:06 2014 +0100
     2.2 +++ b/src/Pure/Isar/parse.scala	Mon Mar 03 11:58:07 2014 +0100
     2.3 @@ -62,9 +62,9 @@
     2.4      def ML_source: Parser[String] = atom("ML source", _.is_text)
     2.5      def document_source: Parser[String] = atom("document source", _.is_text)
     2.6      def path: Parser[String] =
     2.7 -      atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
     2.8 +      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     2.9      def theory_name: Parser[String] =
    2.10 -      atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
    2.11 +      atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content))
    2.12  
    2.13      private def tag_name: Parser[String] =
    2.14        atom("tag name", tok =>
     3.1 --- a/src/Pure/Thy/thy_load.scala	Mon Mar 03 11:37:06 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.scala	Mon Mar 03 11:58:07 2014 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5    def thy_path(path: Path): Path = path.ext("thy")
     3.6  
     3.7 -  def is_ok(str: String): Boolean =
     3.8 +  def is_wellformed(str: String): Boolean =
     3.9      try { thy_path(Path.explode(str)); true }
    3.10      catch { case ERROR(_) => false }
    3.11  }
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:37:06 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:58:07 2014 +0100
     4.3 @@ -181,7 +181,7 @@
     4.4    def hyperlink_source_file(source_name: String, line: Int, raw_offset: Text.Offset)
     4.5      : Option[Hyperlink] =
     4.6    {
     4.7 -    if (Path.is_ok(source_name)) {
     4.8 +    if (Path.is_valid(source_name)) {
     4.9        Isabelle_System.source_file(Path.explode(source_name)) match {
    4.10          case Some(path) =>
    4.11            val name = Isabelle_System.platform_path(path)
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:37:06 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:58:07 2014 +0100
     5.3 @@ -343,7 +343,7 @@
     5.4        range, Vector.empty, Rendering.hyperlink_elements, _ =>
     5.5          {
     5.6            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
     5.7 -          if Path.is_ok(name) =>
     5.8 +          if Path.is_valid(name) =>
     5.9              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    5.10              val link = PIDE.editor.hyperlink_file(jedit_file)
    5.11              Some(links :+ Text.Info(snapshot.convert(info_range), link))
    5.12 @@ -461,7 +461,7 @@
    5.13                else ""
    5.14              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    5.15            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    5.16 -          if Path.is_ok(name) =>
    5.17 +          if Path.is_valid(name) =>
    5.18              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    5.19              Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
    5.20            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>