equal
deleted
inserted
replaced
34 |
34 |
35 fun str_of [] = Context.PureN |
35 fun str_of [] = Context.PureN |
36 | str_of elems = space_implode "/" elems; |
36 | str_of elems = space_implode "/" elems; |
37 |
37 |
38 fun name () = "Isabelle/" ^ str_of (path ()); |
38 fun name () = "Isabelle/" ^ str_of (path ()); |
39 fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")"; |
39 |
|
40 fun welcome () = |
|
41 (if Distribution.is_unofficial then "Unofficial version of " else "Welcome to ") ^ |
|
42 name () ^ " (" ^ Distribution.version ^ ")" ^ |
|
43 (if Distribution.has_changelog then "\nSee ChangeLog.gz for details" else ""); |
40 |
44 |
41 |
45 |
42 (* add_path *) |
46 (* add_path *) |
43 |
47 |
44 fun add_path reset s = |
48 fun add_path reset s = |