Skip to content
Success

Changes

Summary

  1. merged
  2. some updates to README.md;
  3. refer to Isabelle settings via environment, which is provided via "isabelle vscode"; clarified error handling;
  4. more operations;
  5. more robust startup wrt. VSCode workspace (by Fabian Huch);
  6. various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
  7. have Sledgehammer honor 'smt_nat_as_int' option
  8. more handling of Zipperposition definitions in Isar proof construction
  9. handle Zipperposition definitions in Isar proof construction
  10. parse Zipperposition definitions
Changeset 75131:79fab5ff4163 by wenzelm:
merged
Changeset 75130:122d1d1a16fd by wenzelm:
some updates to README.md;
The file was modified src/Tools/VSCode/extension/README.md (diff)
Changeset 75129:49f9fa8f9601 by wenzelm:
refer to Isabelle settings via environment, which is provided via &quot;isabelle vscode&quot;;<br>clarified error handling;
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
Changeset 75128:8c7bdd68a47a by wenzelm:
more operations;
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
Changeset 75127:1fed80019bff by wenzelm:
more robust startup wrt. VSCode workspace (by Fabian Huch);
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts (diff)
Changeset 75126:da1108a6d249 by wenzelm:
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
The file was addedsrc/Tools/VSCode/extension/media/main.js
The file was addedsrc/Tools/VSCode/extension/media/vscode.css
The file was addedsrc/Tools/VSCode/extension/src/abbreviations.ts
The file was addedsrc/Tools/VSCode/extension/src/isabelle_filesystem/isabelle_fsp.ts
The file was addedsrc/Tools/VSCode/extension/src/isabelle_filesystem/prefix_tree.ts
The file was addedsrc/Tools/VSCode/extension/src/isabelle_filesystem/symbol_encoder.ts
The file was addedsrc/Tools/VSCode/extension/src/isabelle_filesystem/uri_map.ts
The file was addedsrc/Tools/VSCode/extension/src/isabelle_filesystem/workspace_state.ts
The file was addedsrc/Tools/VSCode/extension/src/output_view.ts
The file was addedsrc/Tools/VSCode/extension/src/script_decorations.ts
The file was modified CONTRIBUTORS (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/library.ts (diff)
The file was modified src/Tools/VSCode/extension/src/protocol.ts (diff)
The file was modified src/Tools/VSCode/extension/src/state_panel.ts (diff)
The file was modified src/Tools/VSCode/extension/src/symbol.ts (diff)
The file was modified src/Tools/VSCode/extension/test/index.ts (diff)
The file was modified src/Tools/VSCode/extension/tsconfig.json (diff)
The file was modified src/Tools/VSCode/src/dynamic_output.scala (diff)
The file was modified src/Tools/VSCode/src/language_server.scala (diff)
The file was modified src/Tools/VSCode/src/lsp.scala (diff)
The file was modified src/Tools/VSCode/src/state_panel.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 75125:18cd39e55eca by blanchet:
have Sledgehammer honor &#039;smt_nat_as_int&#039; option
The file was modified src/HOL/Tools/ATP/atp_util.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff)
Changeset 75124:f12539c8de0c by blanchet:
more handling of Zipperposition definitions in Isar proof construction
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
Changeset 75123:66eb6fdfc244 by blanchet:
handle Zipperposition definitions in Isar proof construction
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
Changeset 75122:00eeac3fd246 by blanchet:
parse Zipperposition definitions
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)