equal
deleted
inserted
replaced
51 component.load() |
51 component.load() |
52 if (autosave) { |
52 if (autosave) { |
53 component.listenTo(component.selection) |
53 component.listenTo(component.selection) |
54 component.reactions += { case SelectionChanged(_) => component.save() } |
54 component.reactions += { case SelectionChanged(_) => component.save() } |
55 } |
55 } |
56 component.tooltip = Isabelle.options.value.check_name("jedit_logic").print |
56 component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print) |
57 component |
57 component |
58 } |
58 } |
59 |
59 |
60 def session_args(): List[String] = |
60 def session_args(): List[String] = |
61 { |
61 { |