Isabelle/JEdit中do notation对应print mode正确配置问询

你之前尝试的do_notation、do_notations、donotation都不是正确的print mode取值，对应do notation pretty-print的标识为do。

配置生效步骤：

• 打开Isabelle/jEdit顶部菜单栏，依次进入 Plugins > Plugin Options > Isabelle > General
• 找到Print Modes配置栏，在已有配置值的末尾用英文逗号分隔追加do，不要添加多余空格
• 保存配置后重启Isabelle/jEdit，后续输出就会默认显示do notation形式，不再展示展开的bind链式结构

关于所有可用print mode配置项的查询方式：
目前没有单独整理的集中说明文档，你可以通过两个渠道查全所有可用配置：

• 核心内置print mode可以直接查看Isabelle安装目录下src/Pure/Isar/print_mode.ML源码文件，所有内置mode的标识都在该文件中定义，常见的内置项包括ascii、no_brackets、no_symbols以及你需要的do
• 各个加载的第三方理论如果自定义了print mode，会在对应理论源码中通过print_mode命令声明，全局检索工作区源码即可找到对应扩展mode的标识

• 注意：追加do配置时请放在已有print mode列表的末尾，保证该mode的pretty print规则优先级高于默认的monad bind渲染规则，避免配置不生效。

内容的提问来源于stack exchange，提问作者Balazs