equal
deleted
inserted
replaced
74 val PURE = "Pure" |
74 val PURE = "Pure" |
75 val ML_BOOTSTRAP = "ML_Bootstrap" |
75 val ML_BOOTSTRAP = "ML_Bootstrap" |
76 val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") |
76 val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") |
77 val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) |
77 val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) |
78 |
78 |
79 val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE)) |
79 val bootstrap_global_theories = |
|
80 (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) |
80 |
81 |
81 private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") |
82 private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") |
82 private val File_Name = new Regex(""".*?([^/\\:]+)""") |
83 private val File_Name = new Regex(""".*?([^/\\:]+)""") |
83 |
84 |
84 def is_base_name(s: String): Boolean = |
85 def is_base_name(s: String): Boolean = |
92 |
93 |
93 def theory_name(s: String): String = |
94 def theory_name(s: String): String = |
94 s match { |
95 s match { |
95 case Thy_File_Name(name) => bootstrap_name(name) |
96 case Thy_File_Name(name) => bootstrap_name(name) |
96 case File_Name(name) => |
97 case File_Name(name) => |
97 ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") |
98 if (name == Sessions.root_name) name |
|
99 else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") |
98 case _ => "" |
100 case _ => "" |
99 } |
101 } |
100 |
102 |
101 def is_ml_root(theory: String): Boolean = |
103 def is_ml_root(theory: String): Boolean = |
102 ml_roots.exists({ case (_, b) => b == theory }) |
104 ml_roots.exists({ case (_, b) => b == theory }) |