equal
deleted
inserted
replaced
2 ## |
2 ## |
3 ##:encoding=ISO-8859-1: |
3 ##:encoding=ISO-8859-1: |
4 |
4 |
5 #identification |
5 #identification |
6 plugin.isabelle.jedit.Plugin.name=Isabelle |
6 plugin.isabelle.jedit.Plugin.name=Isabelle |
7 plugin.isabelle.jedit.Plugin.author=Johannes H�lzl, Fabian Immler, Makarius Wenzel |
7 plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel |
8 plugin.isabelle.jedit.Plugin.version=0.0.1 |
8 plugin.isabelle.jedit.Plugin.version=0.0.1 |
9 plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing |
9 plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing |
10 |
10 |
11 #system parameters |
11 #system parameters |
12 # jEdit only needs to load the plugin the first time the user accesses it |
12 # jEdit only needs to load the plugin the first time the user accesses it |