Stream: General

Topic: Bug In isabelle linter: appends "theory" to keyword

Ant S. (May 03 2026 at 20:25):

I recently installed the isabelle linter (for Isabelle2025) and now when I open jEDIT, I get this error in Linter.thy:
"Outer syntax error⌂: command expected,
but identifier endtheory⌂ was found" for the keyword end.

theory Linter
  imports Pure
begin

ML ‹
open Command;

val _ =
  let
    fun get_out s = case s of
        "info" => SOME writeln
      | "warn" => SOME warning
      | "error" => SOME error
      | _ => NONE
    fun write_msgs args =
      case args of
       level :: msg :: args1 =>
          let
           val msg1 = (msg |> XML.parse |> YXML.string_of) handle _ => msg
            val _ = case get_out level of SOME out => out msg1 | NONE => ()
          in write_msgs args1 end
      | _ => ()
  in
    print_function "print_xml"
      (fn {args, ...} =>
        SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
          print_fn = fn _ => fn _ => write_msgs args})
  end;
›

end

Say I change end to "en". I know this is clearly wrong, however, the error I get in jEdit's output window is that "entheory" is not found. For some reason, it keeps on appending the string theory to the end of a file. How do I even being to debug this?

I would post an issue, but this is my first time finding a bug like this so I wasn't sure if it was due to some silly mistake on my part

Fabian Huch (May 04 2026 at 07:46):

The current version is Isabelle2025-2.

Ant S. (May 04 2026 at 07:48):

hmm
Is there a general assumption that a slightly older version of isabelle loses all support the moment a new version is released?

Fabian Huch (May 04 2026 at 07:48):

Yes.

Fabian Huch (May 04 2026 at 07:49):

Though you might be able to run an older version of Isabelle with an older version of tool x as long as they match.

Ant S. (May 04 2026 at 07:49):

Yes. I'm specifically running a version of the linter released for Isabelle2025

Ant S. (May 04 2026 at 07:50):

i haven't yet moved to 2025-2 mostly due to some porting work that is on the backburner

Fabian Huch (May 04 2026 at 07:55):

While that is fine, discussing issues with old versions is not helpful.

Fabian Huch (May 04 2026 at 07:56):

In any case, I see that the same message appears in Isabelle2025-2. But other than this message, everything works fine.

Ant S. (May 04 2026 at 07:57):

I understand.
I'll keep this in mind for any other system queries I have in the future.

Fabian Huch (May 04 2026 at 09:00):

As a further incentive to update: In Isabelle2025-2, you will not see the Linter theory error-highlighted unless you open it.

Ant S. (May 04 2026 at 10:07):

(it auto-opens in 2025, I didn't open it myself)

Ant S. (May 04 2026 at 10:07):

or are you trying to say that Linter.thy isn't opened automatically

Last updated: May 15 2026 at 17:41 UTC