src/Pure/Thy/thy_info.scala
changeset 43652 dcd0b667f73d
parent 43651 511df47bcadc
child 43673 29eb1cd29961
equal deleted inserted replaced
43651:511df47bcadc 43652:dcd0b667f73d
    10 class Thy_Info(thy_load: Thy_Load)
    10 class Thy_Info(thy_load: Thy_Load)
    11 {
    11 {
    12   /* messages */
    12   /* messages */
    13 
    13 
    14   private def show_path(names: List[String]): String =
    14   private def show_path(names: List[String]): String =
    15     names.map(Library.quote).mkString(" via ")
    15     names.map(quote).mkString(" via ")
    16 
    16 
    17   private def cycle_msg(names: List[String]): String =
    17   private def cycle_msg(names: List[String]): String =
    18     "Cyclic dependency of " + show_path(names)
    18     "Cyclic dependency of " + show_path(names)
    19 
    19 
    20   private def required_by(s: String, initiators: List[String]): String =
    20   private def required_by(s: String, initiators: List[String]): String =
    43         val (text, header) =
    43         val (text, header) =
    44           try { thy_load.check_thy(dir1, name) }
    44           try { thy_load.check_thy(dir1, name) }
    45           catch {
    45           catch {
    46             case ERROR(msg) =>
    46             case ERROR(msg) =>
    47               cat_error(msg, "The error(s) above occurred while examining theory " +
    47               cat_error(msg, "The error(s) above occurred while examining theory " +
    48                 Library.quote(name) + required_by("\n", initiators))
    48                 quote(name) + required_by("\n", initiators))
    49           }
    49           }
    50         require_thys(name :: initiators, dir1,
    50         require_thys(name :: initiators, dir1,
    51           deps + (name -> Exn.Res(text, header)), header.imports)
    51           deps + (name -> Exn.Res(text, header)), header.imports)
    52       }
    52       }
    53       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    53       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }