Skip to content
Jenkins
log in
Dashboard
isabelle-nightly-benchmark
#219
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Timings
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Failed
Changes
Summary
re-use options from resources;
moved main state to VSCode_Resources; misc tuning;
re-use resources from session;
clarified Document.length -- independent of text_length;
more robust shutdown;
watcher for file-system events;
tuned comments;
Changeset
64704:08c2d80428ff
by
wenzelm
:
re-use options from resources;
The file was modified
src/Tools/VSCode/src/document_model.scala
(diff)
The file was modified
src/Tools/VSCode/src/server.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
64703:a115391494ed
by
wenzelm
:
moved main state to VSCode_Resources;<br>misc tuning;
The file was modified
src/Tools/VSCode/src/document_model.scala
(diff)
The file was modified
src/Tools/VSCode/src/server.scala
(diff)
The file was modified
src/Tools/VSCode/src/vscode_resources.scala
(diff)
Changeset
64702:d95b9117cb5b
by
wenzelm
:
re-use resources from session;
The file was modified
src/Tools/VSCode/src/document_model.scala
(diff)
The file was modified
src/Tools/VSCode/src/server.scala
(diff)
The file was modified
src/Tools/VSCode/src/vscode_rendering.scala
(diff)
Changeset
64701:931f51fb24ca
by
wenzelm
:
clarified Document.length -- independent of text_length;
The file was modified
src/Pure/PIDE/line.scala
(diff)
Changeset
64700:14deaeaa6476
by
wenzelm
:
more robust shutdown;
The file was modified
src/Pure/General/file_watcher.scala
(diff)
Changeset
64699:218c35908d5f
by
wenzelm
:
watcher for file-system events;
The file was added
src/Pure/General/file_watcher.scala
The file was modified
src/Pure/build-jars
(diff)
Changeset
64698:e022a69db531
by
wenzelm
:
tuned comments;
The file was modified
src/Pure/General/file.ML
(diff)
The file was modified
src/Pure/General/file.scala
(diff)