equal
deleted
inserted
replaced
137 case Some(version) => " (" + version + ")" |
137 case Some(version) => " (" + version + ")" |
138 } |
138 } |
139 |
139 |
140 def isabelle_name(): String = getenv_strict("ISABELLE_NAME") |
140 def isabelle_name(): String = getenv_strict("ISABELLE_NAME") |
141 |
141 |
142 def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading() |
142 def identification(): String = |
|
143 "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() |
143 |
144 |
144 |
145 |
145 /** file-system operations **/ |
146 /** file-system operations **/ |
146 |
147 |
147 /* scala functions */ |
148 /* scala functions */ |