more precise error information for dynamic Scala tools
authorLars Hupel <lars.hupel@mytum.de>
Sun, 17 Jul 2016 11:47:35 +0200
changeset 63519 78401d628718
parent 63518 ae8fd6fe63a1
child 63520 2803d2b8f85d
more precise error information for dynamic Scala tools
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)
+    }
   }