[isabelle-dev] JEdit: type constraints no longer printed by default

[Steffen Juilf Smolka]

In af8ecf09a58c, type constraints are no longer printed by default in JEdit:

ML {*
@{term "f"} 
 |> Type.constraint @{typ "nat => nat"}
 |> Syntax.string_of_term @{context}
 |> writeln
*}

# f

Is this the intended behaviour? It used to be different a couple of month ago. I don't know when it changed exacyly, but I think changeset a6814de45b69 might be responsible for the change.

When setting show_markup to false, the behaviour is like it was in the past:

ML {*
@{term "f"} 
 |> Type.constraint @{typ "nat => nat"}
 |> Syntax.string_of_term (@{context} |> Config.put show_markup false)
 |> writeln
*}

# f∷nat ⇒ nat 

Regards,
Steffen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130110/e961fffd/attachment.html>