search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Output re-tokenized as input #46

Open makarius opened 11 years ago

makarius commented 11 years ago

The prover "Output" is re-tokenized (for Isabelle keywords) as in the manner of input source, but this confuses the content. Example: "help print" where words like "abbreviation" in the text are treated accidentally like keywords.

Note that for rendering prover output, only the formal document markup counts.