# 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), _))) =>