# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# 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)
+    }
   }