2.7.0 (Goal View)

This release adds a new view which displays current goals.

To open this goal view, click the book icon (1 in the screenshot below) or execute the command HOL Light: Show HOL Light Goals. The goal view has several options. Additional options can be shown by clicking the plus icon in the lower right corner of the goal view (2 in the screenshot below).

Full Changelog: 2.6.0...2.7.0

2.6.0

• The HOL Light server terminal supports shell integration (https://code.visualstudio.com/docs/terminal/shell-integration).
• Top level expressions are automatically bound to it when using a HOL Light server.

Full Changelog: 2.5.0...2.6.0

2.5.0

What's Changed

• Improve line editing features for terminals associated with HOL Light servers.
• Add line number directive, add 'Connect to Server' button by @aqjune in #22

Full Changelog: 2.4.0...2.5.0

2.4.0

What's Changed

• Use a new command 'er' when running a tactic in list, minor updates by @aqjune in #20

Full Changelog: 2.3.1...2.4.0

v2.1.2

Notes from v2.1.0:

• Added a HOL Light server which enhances the extension capabilities.
• Improved text highlighting and hover messages with a HOL Light server.
• HOL Light files can be opened as interactive notebooks (a HOL Light server is required).
• A special view with search results (a HOL Light server is required).
• Completion suggestions for imports (e.g., after needs).
• New command HOL Light: Send All Statements before the Cursor Position to REPL:
  evaluate everything up to the cursor position (default shortcut Alt+A).
• New command HOL Light: Set Current Working Directory: sets the current working
  directory of a REPL.
• Removed the configuration option simpleSelection.

v2.1.0

• Added a HOL Light server which enhances the extension capabilities.
• Improved text highlighting and hover messages with a HOL Light server.
• HOL Light files can be opened as interactive notebooks (a HOL Light server is required).
• A special view with search results (a HOL Light server is required).
• Completion suggestions for imports (e.g., after needs).
• New command HOL Light: Send All Statements before the Cursor Position to REPL:
  evaluate everything up to the cursor position (default shortcut Alt+A).
• New command HOL Light: Set Current Working Directory: sets the current working
  directory of a REPL.
• Removed the configuration option simpleSelection.

v2.0.0

All open HOL Light files and their dependencies are parsed and an index of definitions and modules is created. This index is used for autocompletion, hover info messages, and Go to Definition features.

v1.0.0

The first published release. Can be installed directly from https://marketplace.visualstudio.com/items?itemName=monadius.hol-light-simple

v0.3.0

• A new algorithm for selecting statements and HOL terms which correctly handles comments and string literals.
• Improved syntax highlighting for HOL type annotations.