# HG changeset patch # User Lars Hupel # Date 1468748855 -7200 # Node ID 78401d628718ac30829b629bf6fcc0448d32ca1c # Parent ae8fd6fe63a1539de81e367773bd04e2e479730d more precise error information for dynamic Scala tools diff -r ae8fd6fe63a1 -r 78401d628718 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sat Jul 16 19:35:27 2016 +0200 +++ b/src/Pure/System/isabelle_tool.scala Sun Jul 17 11:47:35 2016 +0200 @@ -38,7 +38,16 @@ case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } - catch { case e: ToolBoxError => err(e.toString) } + catch { + case e: ToolBoxError => + if (tool_box.frontEnd.hasErrors) { + val infos = tool_box.frontEnd.infos.toList + val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) + err(msgs.mkString("\n")) + } + else + err(e.toString) + } }