Re: [isabelle-dev] Unexpected auto indent in 13a1081961d2
>> the attached theory is the (unexpected) result of typing its content >> naively and relying on auto indent. >> >> Do others experience the same or is it maybe a settings problem? > > Can you check $ISABELLE_HOME_USER/etc/preferences if there are any > changes on jedit_indent_input, jedit_indent_newline, > jedit_indent_script, jedit_indent_script_limit? > > There is also a section about "Indentation" in the Isabelle/jEdit plugin > options dialog. > > Basically everything should be set to the defaults for the best > experience, although there are sometimes old habits to overcome as usual. > > You can also try http://isabelle.in.tum.de/website-Isabelle2017-RC1 with > its fresh environment. Deleting $ISABELLE_HOME_USER/etc/jedit worked, thanks. Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Unexpected auto indent in 13a1081961d2
On 03/09/17 16:08, Florian Haftmann wrote: > > the attached theory is the (unexpected) result of typing its content > naively and relying on auto indent. > > Do others experience the same or is it maybe a settings problem? Can you check $ISABELLE_HOME_USER/etc/preferences if there are any changes on jedit_indent_input, jedit_indent_newline, jedit_indent_script, jedit_indent_script_limit? There is also a section about "Indentation" in the Isabelle/jEdit plugin options dialog. Basically everything should be set to the defaults for the best experience, although there are sometimes old habits to overcome as usual. You can also try http://isabelle.in.tum.de/website-Isabelle2017-RC1 with its fresh environment. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Unexpected auto indent in 13a1081961d2
Dear all, the attached theory is the (unexpected) result of typing its content naively and relying on auto indent. Do others experience the same or is it maybe a settings problem? Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de theory Foo imports Main begin definition I :: "'a \ 'a" where "I x = x" definition K :: "'b \ 'a \ 'a" where "K x = I" lemma K_apply: "K y x = x" by (simp add: K_def I_def) lemma nonsense: "2 * n div 2 = n" if "even n" for n :: nat proof (cases "even n") case True then show ?thesis by simp next case False with that show ?thesis by simp qed signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
