more precise error information for dynamic Scala tools
authorLars Hupel <lars.hupel@mytum.de>
Sun Jul 17 11:47:35 2016 +0200 (2016-07-17)
changeset 6351978401d628718
parent 63518 ae8fd6fe63a1
child 63520 2803d2b8f85d
more precise error information for dynamic Scala tools
src/Pure/System/isabelle_tool.scala
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Sat Jul 16 19:35:27 2016 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Jul 17 11:47:35 2016 +0200
     1.3 @@ -38,7 +38,16 @@
     1.4          case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
     1.5        }
     1.6      }
     1.7 -    catch { case e: ToolBoxError => err(e.toString) }
     1.8 +    catch {
     1.9 +      case e: ToolBoxError =>
    1.10 +        if (tool_box.frontEnd.hasErrors) {
    1.11 +          val infos = tool_box.frontEnd.infos.toList
    1.12 +          val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
    1.13 +          err(msgs.mkString("\n"))
    1.14 +        }
    1.15 +        else
    1.16 +          err(e.toString)
    1.17 +    }
    1.18    }
    1.19  
    1.20