equal
deleted
inserted
replaced
22 let |
22 let |
23 val prefix = #1 (Library.split_last (Long_Name.explode name)); |
23 val prefix = #1 (Library.split_last (Long_Name.explode name)); |
24 val session = |
24 val session = |
25 (case prefix of |
25 (case prefix of |
26 a :: _ => |
26 a :: _ => |
27 (case ThyInfo.lookup_theory a of |
27 (case Thy_Info.lookup_theory a of |
28 SOME thy => |
28 SOME thy => |
29 (case Present.session_name thy of |
29 (case Present.session_name thy of |
30 "" => [] |
30 "" => [] |
31 | session => [session]) |
31 | session => [session]) |
32 | NONE => []) |
32 | NONE => []) |