# HG changeset patch
# User wenzelm
# Date 1393844287 -3600
# Node ID ac979f750c1ae616e4a0eac038f3f30406055f22
# Parent  6d092a5166f1897ce771049b247e00df88f49a6c
clarified path checks: avoid crash of rendering due to spurious errors;

diff -r 6d092a5166f1 -r ac979f750c1a src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Pure/General/path.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -97,9 +97,12 @@
     new Path(norm_elems(elems.reverse ::: roots))
   }
 
-  def is_ok(str: String): Boolean =
+  def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }
 
+  def is_valid(str: String): Boolean =
+    try { explode(str).expand; true } catch { case ERROR(_) => false }
+
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
diff -r 6d092a5166f1 -r ac979f750c1a src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Pure/Isar/parse.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -62,9 +62,9 @@
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
     def path: Parser[String] =
-      atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
+      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     def theory_name: Parser[String] =
-      atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
+      atom("theory name", tok => tok.is_name && Thy_Load.is_wellformed(tok.content))
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
diff -r 6d092a5166f1 -r ac979f750c1a src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Pure/Thy/thy_load.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -18,7 +18,7 @@
 
   def thy_path(path: Path): Path = path.ext("thy")
 
-  def is_ok(str: String): Boolean =
+  def is_wellformed(str: String): Boolean =
     try { thy_path(Path.explode(str)); true }
     catch { case ERROR(_) => false }
 }
diff -r 6d092a5166f1 -r ac979f750c1a src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -181,7 +181,7 @@
   def hyperlink_source_file(source_name: String, line: Int, raw_offset: Text.Offset)
     : Option[Hyperlink] =
   {
-    if (Path.is_ok(source_name)) {
+    if (Path.is_valid(source_name)) {
       Isabelle_System.source_file(Path.explode(source_name)) match {
         case Some(path) =>
           val name = Isabelle_System.platform_path(path)
diff -r 6d092a5166f1 -r ac979f750c1a src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -343,7 +343,7 @@
       range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
-          if Path.is_ok(name) =>
+          if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
@@ -461,7 +461,7 @@
               else ""
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
-          if Path.is_ok(name) =>
+          if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>