diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,367 +1,367 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" -- "build document in given format: pdf, dvi, false" option document_output : string = "" -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_cartouche : bool = false -- "indicate if the output should be delimited as cartouche" option thy_output_quotes : bool = false -- "indicate if the output should be delimited via double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_source_cartouche : bool = false -- "print original source text rather than internal representation, preserve cartouches" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option timeout_scale : real = 1.0 -- "scale factor for session timeout" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option profiling : string = "" -- "ML profiling (possible values: time, allocations)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_statistics : bool = true -- "ML run-time system statistics" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "PIDE Build" -option pide_build : bool = false +option pide_session : bool = false -- "build session heaps via PIDE" option pide_reports : bool = true -- "report PIDE markup" section "Editor Session" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.3 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Headless Session" option headless_consolidate_delay : real = 15 -- "delay to consolidate status of command evaluation (execution forks)" option headless_prune_delay : real = 60 -- "delay to prune history (delete old versions)" option headless_check_delay : real = 0.5 -- "delay for theory status check during PIDE processing (seconds)" option headless_check_limit : int = 0 -- "maximum number of theory status checks (0 = unlimited)" option headless_nodes_status_delay : real = -1 -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" option headless_watchdog_timeout : real = 600 -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" option headless_commit_cleanup_delay : real = 60 -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" option headless_load_limit : real = 5.0 -- "limit in MB for loaded theory files (0 = unlimited)" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" option ssh_config_dir : string = "$HOME/.ssh" -- "SSH configuration directory" option ssh_config_file : string = "$HOME/.ssh/config" -- "main SSH configuration file" option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" -- "possible SSH identity files (separated by colons)" option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Phabricator" option phabricator_version_arcanist : string = "a5bfb968cd90bb0a14c7067e7a2153d5d6ed48d7" -- "repository version for arcanist" option phabricator_version_phabricator : string = "686e51655bb0f4134780dcc68e0276bc9bd0a4af" -- "repository version for phabricator" section "Theory Export" option export_document : bool = false -- "export document sources to Isabelle/Scala" option export_theory : bool = false -- "export theory content to Isabelle/Scala" option export_standard_proofs : bool = false -- "export standardized proof terms to Isabelle/Scala (not scalable)" option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" option prune_proofs : bool = false -- "prune proof terms after export (do not store in Isabelle/ML)" section "Theory update" option update_inner_syntax_cartouches : bool = false -- "update inner syntax (types, terms, etc.) to use cartouches" option update_mixfix_cartouches : bool = false -- "update mixfix templates to use cartouches instead of double quotes" option update_control_cartouches : bool = false -- "update antiquotations to use control symbol with cartouche argument" option update_path_cartouches : bool = false -- "update file-system paths to use cartouches" section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" section "Isabelle/Scala/ML system channel" option system_channel_address : string = "" option system_channel_password : string = "" diff --git a/etc/settings b/etc/settings --- a/etc/settings +++ b/etc/settings @@ -1,170 +1,172 @@ # -*- shell-script -*- :mode=shellscript: # # Isabelle system settings. # # Important notes: # * See the "system" manual for explanations on Isabelle settings # * User settings go into $ISABELLE_HOME_USER/etc/settings # * DO NOT EDIT the repository copy of this file! # * DO NOT COPY this file into the $ISABELLE_HOME_USER directory! ### ### Isabelle/Scala ### ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" isabelle_scala_service 'isabelle.Tools' [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools' +isabelle_scala_service 'isabelle.Functions' + isabelle_scala_service 'isabelle.Bibtex$File_Format' #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS ### ### Interactive sessions (cf. isabelle console) ### ISABELLE_LINE_EDITOR="rlwrap" ### ### Batch sessions (cf. isabelle build) ### ISABELLE_BUILD_OPTIONS="" ### ### Document preparation (cf. isabelle latex/document) ### ISABELLE_LATEX="latex -file-line-error" ISABELLE_PDFLATEX="pdflatex -file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex" ISABELLE_EPSTOPDF="epstopdf" if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then ISABELLE_LATEX="latex -c-style-errors" ISABELLE_PDFLATEX="pdflatex -c-style-errors" fi ### ### Misc path settings ### ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components" ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib" # The place for user configuration, heap files, etc. if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER" fi # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER" # Heap locations. ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } ISABELLE_SITE_SETTINGS_PRESENT=true ### ### Default logic ### ISABELLE_LOGIC=HOL ### ### Docs ### # Where to look for docs (multiple dirs separated by ':'). ISABELLE_DOCS="$ISABELLE_HOME/doc" ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY" ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML" # "open" within desktop environment (potentially asynchronous) case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_OPEN="xdg-open" ;; macos) ISABELLE_OPEN="open" ;; windows) ISABELLE_OPEN="cygstart" ;; esac PDF_VIEWER="$ISABELLE_OPEN" DVI_VIEWER="$ISABELLE_OPEN" ### ### Symbol rendering ### ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" ### ### OCaml ### ISABELLE_OPAM_ROOT="$USER_HOME/.opam" ISABELLE_OCAML_VERSION="ocaml-base-compiler.4.05.0" ### ### Haskell ### ISABELLE_STACK_ROOT="$USER_HOME/.stack" ISABELLE_STACK_RESOLVER="lts-13.19" ISABELLE_GHC_VERSION="ghc-8.6.4" ### ### Misc settings ### ISABELLE_GNUPLOT="gnuplot" ISABELLE_FONTFORGE="fontforge" #ISABELLE_MLTON="/usr/bin/mlton" #ISABELLE_SMLNJ="/usr/bin/sml" #ISABELLE_SWIPL="/usr/bin/swipl" diff --git a/etc/symbols b/etc/symbols --- a/etc/symbols +++ b/etc/symbols @@ -1,436 +1,438 @@ # Default interpretation of some Isabelle symbols \ code: 0x01d7ec group: digit \ code: 0x01d7ed group: digit \ code: 0x01d7ee group: digit \ code: 0x01d7ef group: digit \ code: 0x01d7f0 group: digit \ code: 0x01d7f1 group: digit \ code: 0x01d7f2 group: digit \ code: 0x01d7f3 group: digit \ code: 0x01d7f4 group: digit \ code: 0x01d7f5 group: digit \ code: 0x01d49c group: letter \ code: 0x00212c group: letter \ code: 0x01d49e group: letter \ code: 0x01d49f group: letter \ code: 0x002130 group: letter \ code: 0x002131 group: letter \ code: 0x01d4a2 group: letter \ code: 0x00210b group: letter \ code: 0x002110 group: letter \ code: 0x01d4a5 group: letter \ code: 0x01d4a6 group: letter \ code: 0x002112 group: letter \ code: 0x002133 group: letter \ code: 0x01d4a9 group: letter \ code: 0x01d4aa group: letter \

code: 0x01d5c9 group: letter \ code: 0x01d5ca group: letter \ code: 0x01d5cb group: letter \ code: 0x01d5cc group: letter \ code: 0x01d5cd group: letter \ code: 0x01d5ce group: letter \ code: 0x01d5cf group: letter \ code: 0x01d5d0 group: letter \ code: 0x01d5d1 group: letter \ code: 0x01d5d2 group: letter \ code: 0x01d5d3 group: letter \ code: 0x01d504 group: letter \ code: 0x01d505 group: letter \ code: 0x00212d group: letter \

code: 0x01d507 group: letter \ code: 0x01d508 group: letter \ code: 0x01d509 group: letter \ code: 0x01d50a group: letter \ code: 0x00210c group: letter \ code: 0x002111 group: letter \ code: 0x01d50d group: letter \ code: 0x01d50e group: letter \ code: 0x01d50f group: letter \ code: 0x01d510 group: letter \ code: 0x01d511 group: letter \ code: 0x01d512 group: letter \ code: 0x01d513 group: letter \ code: 0x01d514 group: letter \ code: 0x00211c group: letter \ code: 0x01d516 group: letter \ code: 0x01d517 group: letter \ code: 0x01d518 group: letter \ code: 0x01d519 group: letter \ code: 0x01d51a group: letter \ code: 0x01d51b group: letter \ code: 0x01d51c group: letter \ code: 0x002128 group: letter \ code: 0x01d51e group: letter \ code: 0x01d51f group: letter \ code: 0x01d520 group: letter \
code: 0x01d521 group: letter \ code: 0x01d522 group: letter \ code: 0x01d523 group: letter \ code: 0x01d524 group: letter \ code: 0x01d525 group: letter \ code: 0x01d526 group: letter \ code: 0x01d527 group: letter \ code: 0x01d528 group: letter \ code: 0x01d529 group: letter \ code: 0x01d52a group: letter \ code: 0x01d52b group: letter \ code: 0x01d52c group: letter \ code: 0x01d52d group: letter \ code: 0x01d52e group: letter \ code: 0x01d52f group: letter \ code: 0x01d530 group: letter \ code: 0x01d531 group: letter \ code: 0x01d532 group: letter \ code: 0x01d533 group: letter \ code: 0x01d534 group: letter \ code: 0x01d535 group: letter \ code: 0x01d536 group: letter \ code: 0x01d537 group: letter \ code: 0x0003b1 group: greek \ code: 0x0003b2 group: greek \ code: 0x0003b3 group: greek \ code: 0x0003b4 group: greek \ code: 0x0003b5 group: greek \ code: 0x0003b6 group: greek \ code: 0x0003b7 group: greek \ code: 0x0003b8 group: greek \ code: 0x0003b9 group: greek \ code: 0x0003ba group: greek \ code: 0x0003bb group: greek abbrev: % \ code: 0x0003bc group: greek \ code: 0x0003bd group: greek \ code: 0x0003be group: greek \ code: 0x0003c0 group: greek \ code: 0x0003c1 group: greek \ code: 0x0003c3 group: greek \ code: 0x0003c4 group: greek \ code: 0x0003c5 group: greek \ code: 0x0003c6 group: greek \ code: 0x0003c7 group: greek \ code: 0x0003c8 group: greek \ code: 0x0003c9 group: greek \ code: 0x000393 group: greek \ code: 0x000394 group: greek \ code: 0x000398 group: greek \ code: 0x00039b group: greek \ code: 0x00039e group: greek \ code: 0x0003a0 group: greek \ code: 0x0003a3 group: greek \ code: 0x0003a5 group: greek \ code: 0x0003a6 group: greek \ code: 0x0003a8 group: greek \ code: 0x0003a9 group: greek \ code: 0x01d539 group: letter \ code: 0x002102 group: letter \ code: 0x002115 group: letter \ code: 0x00211a group: letter \ code: 0x00211d group: letter \ code: 0x002124 group: letter \ code: 0x002190 group: arrow abbrev: <. \ code: 0x0027f5 group: arrow abbrev: <. \ code: 0x00290e group: arrow abbrev: <. \ code: 0x0021e0 group: arrow abbrev: <. \ code: 0x002192 group: arrow abbrev: .> abbrev: -> \ code: 0x0027f6 group: arrow abbrev: .> abbrev: --> \ code: 0x00290f group: arrow abbrev: .> abbrev: ---> \ code: 0x0021e2 group: arrow abbrev: .> abbrev: ---> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. \ code: 0x0021da group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => \ code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> \ code: 0x0021db group: arrow abbrev: .> \ code: 0x002194 group: arrow abbrev: <> abbrev: <-> \ code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> \ code: 0x0021d4 group: arrow abbrev: <> \ code: 0x0027fa group: arrow abbrev: <> \ code: 0x0021a6 group: arrow abbrev: .> abbrev: |-> \ code: 0x0027fc group: arrow abbrev: .> abbrev: |--> \ code: 0x002500 group: arrow abbrev: <> \ code: 0x002550 group: arrow abbrev: <> \ code: 0x0021a9 group: arrow abbrev: <. \ code: 0x0021aa group: arrow abbrev: .> \ code: 0x0021bd group: arrow abbrev: <. \ code: 0x0021c1 group: arrow abbrev: .> \ code: 0x0021bc group: arrow abbrev: <. \ code: 0x0021c0 group: arrow abbrev: .> \ code: 0x0021cc group: arrow abbrev: <> abbrev: == \ code: 0x00219d group: arrow abbrev: .> abbrev: ~> \ code: 0x0021c3 group: arrow \ code: 0x0021c2 group: arrow \ code: 0x0021bf group: arrow #\ code: 0x0021be group: arrow \ code: 0x0021be group: operator \ code: 0x002237 group: punctuation \ code: 0x002191 group: arrow \ code: 0x0021d1 group: arrow \ code: 0x002193 group: arrow \ code: 0x0021d3 group: arrow \ code: 0x002195 group: arrow \ code: 0x0021d5 group: arrow \ code: 0x0027e8 group: punctuation abbrev: << \ code: 0x0027e9 group: punctuation abbrev: >> \ code: 0x0027ea group: punctuation abbrev: << \ code: 0x0027eb group: punctuation abbrev: >> \ code: 0x002308 group: punctuation abbrev: [. \ code: 0x002309 group: punctuation abbrev: .] \ code: 0x00230a group: punctuation abbrev: [. \ code: 0x00230b group: punctuation abbrev: .] \ code: 0x002987 group: punctuation abbrev: (| \ code: 0x002988 group: punctuation abbrev: |) \ code: 0x0027e6 group: punctuation abbrev: [| \ code: 0x0027e7 group: punctuation abbrev: |] \ code: 0x002983 group: punctuation abbrev: {| \ code: 0x002984 group: punctuation abbrev: |} \ code: 0x0000ab group: punctuation abbrev: << \ code: 0x0000bb group: punctuation abbrev: >> \ code: 0x0022a5 group: logic \ code: 0x0022a4 group: logic \ code: 0x002227 group: logic abbrev: /\ abbrev: & \ code: 0x0022c0 group: logic abbrev: !! \ code: 0x002228 group: logic abbrev: \/ abbrev: | \ code: 0x0022c1 group: logic abbrev: ?? \ code: 0x002200 group: logic abbrev: ! abbrev: ALL \ code: 0x002203 group: logic abbrev: ? abbrev: EX \ code: 0x002204 group: logic abbrev: ~? \ code: 0x0000ac group: logic abbrev: ~ \ code: 0x0025cb group: logic \ code: 0x0025a1 group: logic \ code: 0x0025c7 group: logic \ code: 0x0022c4 group: operator \ code: 0x0022a2 group: relation abbrev: |- \ code: 0x0022a8 group: relation abbrev: |= \ code: 0x0022a9 group: relation abbrev: |- \ code: 0x0022ab group: relation abbrev: |= \ code: 0x0022a3 group: relation abbrev: -| \ code: 0x00221a group: relation \ code: 0x002264 group: relation abbrev: <= \ code: 0x002265 group: relation abbrev: >= \ code: 0x00226a group: relation abbrev: << \ code: 0x00226b group: relation abbrev: >> \ code: 0x002272 group: relation \ code: 0x002273 group: relation \ code: 0x002a85 group: relation \ code: 0x002a86 group: relation \ code: 0x002208 group: relation abbrev: : \ code: 0x002209 group: relation abbrev: ~: \ code: 0x002282 group: relation \ code: 0x002283 group: relation \ code: 0x002286 group: relation abbrev: (= \ code: 0x002287 group: relation abbrev: )= \ code: 0x00228f group: relation \ code: 0x002290 group: relation \ code: 0x002291 group: relation abbrev: [= \ code: 0x002292 group: relation abbrev: ]= \ code: 0x002229 group: operator abbrev: Int \ code: 0x0022c2 group: operator abbrev: Inter abbrev: INT \ code: 0x00222a group: operator abbrev: Un \ code: 0x0022c3 group: operator abbrev: Union abbrev: UN \ code: 0x002294 group: operator \ code: 0x002a06 group: operator abbrev: SUP \ code: 0x002293 group: operator \ code: 0x002a05 group: operator abbrev: INF \ code: 0x002216 group: operator \ code: 0x00221d group: operator \ code: 0x00228e group: operator \ code: 0x002a04 group: operator \ code: 0x002260 group: relation abbrev: ~= \ code: 0x00223c group: relation \ code: 0x002250 group: relation abbrev: .= \ code: 0x002243 group: relation \ code: 0x002248 group: relation \ code: 0x00224d group: relation \ code: 0x002245 group: relation \ code: 0x002323 group: relation \ code: 0x002261 group: relation abbrev: == \ code: 0x002322 group: relation \ code: 0x0022c8 \ code: 0x002a1d \ code: 0x00227a group: relation \ code: 0x00227b group: relation \ code: 0x00227c group: relation \ code: 0x00227d group: relation \ code: 0x002225 group: punctuation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || \ code: 0x002aff group: punctuation abbrev: || \ code: 0x0000b1 group: operator \ code: 0x002213 group: operator \ code: 0x0000d7 group: operator abbrev: <*> \
code: 0x0000f7 group: operator \ code: 0x0022c5 group: operator \ code: 0x0022c6 group: operator \ code: 0x002219 group: operator \ code: 0x002218 group: operator \ code: 0x002020 \ code: 0x002021 \ code: 0x0022b2 group: relation \ code: 0x0022b3 group: relation \ code: 0x0022b4 group: relation \ code: 0x0022b5 group: relation \ code: 0x0025c3 group: relation \ code: 0x0025b9 group: relation \ code: 0x0025b3 group: relation \ code: 0x00225c group: relation \ code: 0x002295 group: operator \ code: 0x002a01 group: operator \ code: 0x002297 group: operator \ code: 0x002a02 group: operator \ code: 0x002299 group: operator \ code: 0x002a00 group: operator \ code: 0x002296 group: operator \ code: 0x002298 group: operator \ code: 0x002026 group: punctuation abbrev: ... \ code: 0x0022ef group: punctuation \ code: 0x002211 group: operator abbrev: SUM \ code: 0x00220f group: operator abbrev: PROD \ code: 0x002210 group: operator \ code: 0x00221e \ code: 0x00222b group: operator \ code: 0x00222e group: operator \ code: 0x002663 \ code: 0x002662 \ code: 0x002661 \ code: 0x002660 \ code: 0x002135 \ code: 0x002205 \ code: 0x002207 \ code: 0x002202 \ code: 0x00266d \ code: 0x00266e \ code: 0x00266f \ code: 0x002220 \ code: 0x0000a9 \ code: 0x0000ae \ code: 0x002010 group: punctuation \ code: 0x0000af group: operator \ code: 0x0000b7 group: punctuation \ code: 0x0000bc group: digit \ code: 0x0000bd group: digit \ code: 0x0000be group: digit \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 \ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac \ code: 0x0000a3 \ code: 0x0000a5 \ code: 0x0000a2 \ code: 0x0000a4 \ code: 0x0000b0 \ code: 0x002a3f group: operator \ code: 0x002127 group: operator \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 group: relation \ code: 0x0000b4 \ code: 0x000131 \ code: 0x0000a8 \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x00291c group: operator abbrev: >>= \ code: 0x002aa2 group: operator abbrev: >> \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce \ code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^latex> group: document argument: cartouche \<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \ code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: << \ code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >> \<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono \<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono \<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_( \<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_) \<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^( \<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^) \<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^assert> \<^binding> argument: cartouche \<^class> argument: cartouche \<^class_syntax> argument: cartouche \<^command_keyword> argument: cartouche \<^const> argument: cartouche \<^const_abbrev> argument: cartouche \<^const_name> argument: cartouche \<^const_syntax> argument: cartouche \<^context> \<^cprop> argument: cartouche \<^cterm> argument: cartouche \<^ctyp> argument: cartouche \<^keyword> argument: cartouche \<^locale> argument: cartouche \<^make_string> \<^method> argument: cartouche \<^named_theorems> argument: cartouche \<^nonterminal> argument: cartouche \<^path> argument: cartouche \<^path_binding> argument: cartouche \<^plugin> argument: cartouche \<^print> \<^prop> argument: cartouche +\<^scala> argument: cartouche +\<^scala_function> argument: cartouche \<^session> argument: cartouche \<^simproc> argument: cartouche \<^sort> argument: cartouche \<^syntax_const> argument: cartouche \<^system_option> argument: cartouche \<^term> argument: cartouche \<^theory> argument: cartouche \<^theory_context> argument: cartouche \<^typ> argument: cartouche \<^type_abbrev> argument: cartouche \<^type_name> argument: cartouche \<^type_syntax> argument: cartouche \<^oracle_name> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche \<^computation_check> argument: cartouche diff --git a/lib/Tools/scala b/lib/Tools/scala --- a/lib/Tools/scala +++ b/lib/Tools/scala @@ -1,17 +1,21 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: invoke Scala within the Isabelle environment isabelle_admin_build jars || exit $? eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)" declare -a SCALA_ARGS=() for ARG in "${JAVA_ARGS[@]}" do SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG" done +[ -n "$CLASSPATH" ] && classpath "$CLASSPATH" +unset CLASSPATH + isabelle_scala scala "${SCALA_ARGS[@]}" \ - -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@" + -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \ + -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@" diff --git a/lib/texinputs/isabellesym.sty b/lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty +++ b/lib/texinputs/isabellesym.sty @@ -1,421 +1,423 @@ %% %% definitions of standard Isabelle symbols %% \newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb \newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb \newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb \newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb \newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb \newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb \newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb \newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb \newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb \newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb \newcommand{\isasymA}{\isamath{\mathcal{A}}} \newcommand{\isasymB}{\isamath{\mathcal{B}}} \newcommand{\isasymC}{\isamath{\mathcal{C}}} \newcommand{\isasymD}{\isamath{\mathcal{D}}} \newcommand{\isasymE}{\isamath{\mathcal{E}}} \newcommand{\isasymF}{\isamath{\mathcal{F}}} \newcommand{\isasymG}{\isamath{\mathcal{G}}} \newcommand{\isasymH}{\isamath{\mathcal{H}}} \newcommand{\isasymI}{\isamath{\mathcal{I}}} \newcommand{\isasymJ}{\isamath{\mathcal{J}}} \newcommand{\isasymK}{\isamath{\mathcal{K}}} \newcommand{\isasymL}{\isamath{\mathcal{L}}} \newcommand{\isasymM}{\isamath{\mathcal{M}}} \newcommand{\isasymN}{\isamath{\mathcal{N}}} \newcommand{\isasymO}{\isamath{\mathcal{O}}} \newcommand{\isasymP}{\isamath{\mathcal{P}}} \newcommand{\isasymQ}{\isamath{\mathcal{Q}}} \newcommand{\isasymR}{\isamath{\mathcal{R}}} \newcommand{\isasymS}{\isamath{\mathcal{S}}} \newcommand{\isasymT}{\isamath{\mathcal{T}}} \newcommand{\isasymU}{\isamath{\mathcal{U}}} \newcommand{\isasymV}{\isamath{\mathcal{V}}} \newcommand{\isasymW}{\isamath{\mathcal{W}}} \newcommand{\isasymX}{\isamath{\mathcal{X}}} \newcommand{\isasymY}{\isamath{\mathcal{Y}}} \newcommand{\isasymZ}{\isamath{\mathcal{Z}}} \newcommand{\isasyma}{\isamath{\mathrm{a}}} \newcommand{\isasymb}{\isamath{\mathrm{b}}} \newcommand{\isasymc}{\isamath{\mathrm{c}}} \newcommand{\isasymd}{\isamath{\mathrm{d}}} \newcommand{\isasyme}{\isamath{\mathrm{e}}} \newcommand{\isasymf}{\isamath{\mathrm{f}}} \newcommand{\isasymg}{\isamath{\mathrm{g}}} \newcommand{\isasymh}{\isamath{\mathrm{h}}} \newcommand{\isasymi}{\isamath{\mathrm{i}}} \newcommand{\isasymj}{\isamath{\mathrm{j}}} \newcommand{\isasymk}{\isamath{\mathrm{k}}} \newcommand{\isasyml}{\isamath{\mathrm{l}}} \newcommand{\isasymm}{\isamath{\mathrm{m}}} \newcommand{\isasymn}{\isamath{\mathrm{n}}} \newcommand{\isasymo}{\isamath{\mathrm{o}}} \newcommand{\isasymp}{\isamath{\mathrm{p}}} \newcommand{\isasymq}{\isamath{\mathrm{q}}} \newcommand{\isasymr}{\isamath{\mathrm{r}}} \newcommand{\isasyms}{\isamath{\mathrm{s}}} \newcommand{\isasymt}{\isamath{\mathrm{t}}} \newcommand{\isasymu}{\isamath{\mathrm{u}}} \newcommand{\isasymv}{\isamath{\mathrm{v}}} \newcommand{\isasymw}{\isamath{\mathrm{w}}} \newcommand{\isasymx}{\isamath{\mathrm{x}}} \newcommand{\isasymy}{\isamath{\mathrm{y}}} \newcommand{\isasymz}{\isamath{\mathrm{z}}} \newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak \newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak \newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak \newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak \newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak \newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak \newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak \newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak \newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak \newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak \newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak \newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak \newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak \newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak \newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak \newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak \newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak \newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak \newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak \newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak \newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak \newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak \newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak \newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak \newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak \newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak \newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak \newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak \newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak \newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak \newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak \newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak \newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak \newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak \newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak \newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak \newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak \newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak \newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak \newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak \newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak \newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak \newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak \newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak \newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak \newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak \newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak \newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak \newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak \newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak \newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak \newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak \newcommand{\isasymalpha}{\isamath{\alpha}} \newcommand{\isasymbeta}{\isamath{\beta}} \newcommand{\isasymgamma}{\isamath{\gamma}} \newcommand{\isasymdelta}{\isamath{\delta}} \newcommand{\isasymepsilon}{\isamath{\varepsilon}} \newcommand{\isasymzeta}{\isamath{\zeta}} \newcommand{\isasymeta}{\isamath{\eta}} \newcommand{\isasymtheta}{\isamath{\vartheta}} \newcommand{\isasymiota}{\isamath{\iota}} \newcommand{\isasymkappa}{\isamath{\kappa}} \newcommand{\isasymlambda}{\isamath{\lambda}} \newcommand{\isasymmu}{\isamath{\mu}} \newcommand{\isasymnu}{\isamath{\nu}} \newcommand{\isasymxi}{\isamath{\xi}} \newcommand{\isasympi}{\isamath{\pi}} \newcommand{\isasymrho}{\isamath{\varrho}} \newcommand{\isasymsigma}{\isamath{\sigma}} \newcommand{\isasymtau}{\isamath{\tau}} \newcommand{\isasymupsilon}{\isamath{\upsilon}} \newcommand{\isasymphi}{\isamath{\varphi}} \newcommand{\isasymchi}{\isamath{\chi}} \newcommand{\isasympsi}{\isamath{\psi}} \newcommand{\isasymomega}{\isamath{\omega}} \newcommand{\isasymGamma}{\isamath{\Gamma}} \newcommand{\isasymDelta}{\isamath{\Delta}} \newcommand{\isasymTheta}{\isamath{\Theta}} \newcommand{\isasymLambda}{\isamath{\Lambda}} \newcommand{\isasymXi}{\isamath{\Xi}} \newcommand{\isasymPi}{\isamath{\Pi}} \newcommand{\isasymSigma}{\isamath{\Sigma}} \newcommand{\isasymUpsilon}{\isamath{\Upsilon}} \newcommand{\isasymPhi}{\isamath{\Phi}} \newcommand{\isasymPsi}{\isamath{\Psi}} \newcommand{\isasymOmega}{\isamath{\Omega}} \newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}} \newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}} \newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}} \newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}} \newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}} \newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}} \newcommand{\isasymleftarrow}{\isamath{\leftarrow}} \newcommand{\isasymrightarrow}{\isamath{\rightarrow}} \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} \newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} \newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} \newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} \newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb \newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb \newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} \newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} \newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} \newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}} \newcommand{\isasymmapsto}{\isamath{\mapsto}} \newcommand{\isasymlongmapsto}{\isamath{\longmapsto}} \newcommand{\isasymmidarrow}{\isamath{\relbar}} \newcommand{\isasymMidarrow}{\isamath{\Relbar}} \newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}} \newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}} \newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}} \newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}} \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}} \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}} \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} \newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb \newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb \newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb \newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb \newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb \newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb \newcommand{\isasymColon}{\isamath{\mathrel{::}}} \newcommand{\isasymup}{\isamath{\uparrow}} \newcommand{\isasymUp}{\isamath{\Uparrow}} \newcommand{\isasymdown}{\isamath{\downarrow}} \newcommand{\isasymDown}{\isamath{\Downarrow}} \newcommand{\isasymupdown}{\isamath{\updownarrow}} \newcommand{\isasymUpdown}{\isamath{\Updownarrow}} \newcommand{\isasymlangle}{\isamath{\langle}} \newcommand{\isasymrangle}{\isamath{\rangle}} \newcommand{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}} \newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}} \newcommand{\isasymlceil}{\isamath{\lceil}} \newcommand{\isasymrceil}{\isamath{\rceil}} \newcommand{\isasymlfloor}{\isamath{\lfloor}} \newcommand{\isasymrfloor}{\isamath{\rfloor}} \newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}} \newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}} \newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} \newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} \newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}} \newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}} \newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel \newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel \newcommand{\isasymbottom}{\isamath{\bot}} \newcommand{\isasymtop}{\isamath{\top}} \newcommand{\isasymand}{\isamath{\wedge}} \newcommand{\isasymAnd}{\isamath{\bigwedge}} \newcommand{\isasymor}{\isamath{\vee}} \newcommand{\isasymOr}{\isamath{\bigvee}} \newcommand{\isasymforall}{\isamath{\forall\,}} \newcommand{\isasymexists}{\isamath{\exists\,}} \newcommand{\isasymnot}{\isamath{\neg}} \newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb \newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym \newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb \newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb \newcommand{\isasymdiamondop}{\isamath{\diamond}} \newcommand{\isasymsurd}{\isamath{\surd}} \newcommand{\isasymturnstile}{\isamath{\vdash}} \newcommand{\isasymTurnstile}{\isamath{\models}} \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} \newcommand{\isasymstileturn}{\isamath{\dashv}} \newcommand{\isasymle}{\isamath{\le}} \newcommand{\isasymge}{\isamath{\ge}} \newcommand{\isasymlless}{\isamath{\ll}} \newcommand{\isasymggreater}{\isamath{\gg}} \newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb \newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb \newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb \newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb \newcommand{\isasymin}{\isamath{\in}} \newcommand{\isasymnotin}{\isamath{\notin}} \newcommand{\isasymsubset}{\isamath{\subset}} \newcommand{\isasymsupset}{\isamath{\supset}} \newcommand{\isasymsubseteq}{\isamath{\subseteq}} \newcommand{\isasymsupseteq}{\isamath{\supseteq}} \newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb \newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} \newcommand{\isasyminter}{\isamath{\cap}} \newcommand{\isasymInter}{\isamath{\bigcap\,}} \newcommand{\isasymunion}{\isamath{\cup}} \newcommand{\isasymUnion}{\isamath{\bigcup\,}} \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} \newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymsetminus}{\isamath{\setminus}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymuplus}{\isamath{\uplus}} \newcommand{\isasymUplus}{\isamath{\biguplus\,}} \newcommand{\isasymnoteq}{\isamath{\not=}} \newcommand{\isasymsim}{\isamath{\sim}} \newcommand{\isasymdoteq}{\isamath{\doteq}} \newcommand{\isasymsimeq}{\isamath{\simeq}} \newcommand{\isasymapprox}{\isamath{\approx}} \newcommand{\isasymasymp}{\isamath{\asymp}} \newcommand{\isasymcong}{\isamath{\cong}} \newcommand{\isasymsmile}{\isamath{\smile}} \newcommand{\isasymequiv}{\isamath{\equiv}} \newcommand{\isasymfrown}{\isamath{\frown}} \newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb \newcommand{\isasymbowtie}{\isamath{\bowtie}} \newcommand{\isasymprec}{\isamath{\prec}} \newcommand{\isasymsucc}{\isamath{\succ}} \newcommand{\isasympreceq}{\isamath{\preceq}} \newcommand{\isasymsucceq}{\isamath{\succeq}} \newcommand{\isasymparallel}{\isamath{\parallel}} \newcommand{\isasymbar}{\isamath{\mid}} \newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}} \newcommand{\isasymplusminus}{\isamath{\pm}} \newcommand{\isasymminusplus}{\isamath{\mp}} \newcommand{\isasymtimes}{\isamath{\times}} \newcommand{\isasymdiv}{\isamath{\div}} \newcommand{\isasymcdot}{\isamath{\cdot}} \newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb \newcommand{\isasymstar}{\isamath{\star}} \newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}} \newcommand{\isasymcirc}{\isamath{\circ}} \newcommand{\isasymdagger}{\isamath{\dagger}} \newcommand{\isasymddagger}{\isamath{\ddagger}} \newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb \newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb \newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb \newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}} \newcommand{\isasymtriangleright}{\isamath{\triangleright}} \newcommand{\isasymtriangle}{\isamath{\triangle}} \newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb \newcommand{\isasymoplus}{\isamath{\oplus}} \newcommand{\isasymOplus}{\isamath{\bigoplus\,}} \newcommand{\isasymotimes}{\isamath{\otimes}} \newcommand{\isasymOtimes}{\isamath{\bigotimes\,}} \newcommand{\isasymodot}{\isamath{\odot}} \newcommand{\isasymOdot}{\isamath{\bigodot\,}} \newcommand{\isasymominus}{\isamath{\ominus}} \newcommand{\isasymoslash}{\isamath{\oslash}} \newcommand{\isasymdots}{\isamath{\dots}} \newcommand{\isasymcdots}{\isamath{\cdots}} \newcommand{\isasymSum}{\isamath{\sum\,}} \newcommand{\isasymProd}{\isamath{\prod\,}} \newcommand{\isasymCoprod}{\isamath{\coprod\,}} \newcommand{\isasyminfinity}{\isamath{\infty}} \newcommand{\isasymintegral}{\isamath{\int\,}} \newcommand{\isasymointegral}{\isamath{\oint\,}} \newcommand{\isasymclubsuit}{\isamath{\clubsuit}} \newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}} \newcommand{\isasymheartsuit}{\isamath{\heartsuit}} \newcommand{\isasymspadesuit}{\isamath{\spadesuit}} \newcommand{\isasymaleph}{\isamath{\aleph}} \newcommand{\isasymemptyset}{\isamath{\emptyset}} \newcommand{\isasymnabla}{\isamath{\nabla}} \newcommand{\isasympartial}{\isamath{\partial}} \newcommand{\isasymRe}{\isamath{\Re}} \newcommand{\isasymIm}{\isamath{\Im}} \newcommand{\isasymflat}{\isamath{\flat}} \newcommand{\isasymnatural}{\isamath{\natural}} \newcommand{\isasymsharp}{\isamath{\sharp}} \newcommand{\isasymangle}{\isamath{\angle}} \newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}} \newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}} \newcommand{\isasyminverse}{\isamath{{}^{-1}}} \newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp \newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp \newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp \newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}} \newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}} \newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}} \newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}} \newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}} \newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}} \newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym \newcommand{\isasympounds}{\isamath{\pounds}} \newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb \newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp \newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}} %requires textcomp \newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}} \newcommand{\isasymamalg}{\isamath{\amalg}} \newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb \newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb \newcommand{\isasymwp}{\isamath{\wp}} \newcommand{\isasymwrong}{\isamath{\wr}} \newcommand{\isasymacute}{\isatext{\'\relax}} \newcommand{\isasymindex}{\isatext{\i}} \newcommand{\isasymdieresis}{\isatext{\"\relax}} \newcommand{\isasymcedilla}{\isatext{\c\relax}} \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}} \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}} \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymcomment}{\isatext{\isastylecmt---}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} \newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont \newcommand{\isactrlassert}{\isakeywordcontrol{assert}} \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}} \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} \newcommand{\isactrlclass}{\isakeywordcontrol{class}} \newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} \newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} \newcommand{\isactrlconst}{\isakeywordcontrol{const}} \newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} \newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} \newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} \newcommand{\isactrlcontext}{\isakeywordcontrol{context}} \newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} \newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} \newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} \newcommand{\isactrldir}{\isakeywordcontrol{dir}} \newcommand{\isactrlfile}{\isakeywordcontrol{file}} \newcommand{\isactrlhere}{\isakeywordcontrol{here}} \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} \newcommand{\isactrllatex}{\isakeywordcontrol{latex}} \newcommand{\isactrllocale}{\isakeywordcontrol{locale}} \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}} \newcommand{\isactrlmethod}{\isakeywordcontrol{method}} \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} \newcommand{\isactrlpath}{\isakeywordcontrol{path}} \newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} \newcommand{\isactrlprint}{\isakeywordcontrol{print}} \newcommand{\isactrlprop}{\isakeywordcontrol{prop}} +\newcommand{\isactrlscala}{\isakeywordcontrol{scala}} +\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}} \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} \newcommand{\isactrlsort}{\isakeywordcontrol{sort}} \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} \newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} \newcommand{\isactrlterm}{\isakeywordcontrol{term}} \newcommand{\isactrltheory}{\isakeywordcontrol{theory}} \newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} \newcommand{\isactrltyp}{\isakeywordcontrol{typ}} \newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} \newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} \newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} \newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} \newcommand{\isactrlcode}{\isakeywordcontrol{code}} \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} \newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} \newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} diff --git a/src/Pure/Concurrent/future.ML b/src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML +++ b/src/Pure/Concurrent/future.ML @@ -1,719 +1,717 @@ (* Title: Pure/Concurrent/future.ML Author: Makarius Value-oriented parallel execution via futures and promises. *) signature FUTURE = sig type task = Task_Queue.task type group = Task_Queue.group val new_group: group option -> group val worker_task: unit -> task option val worker_group: unit -> group option val the_worker_group: unit -> group val worker_subgroup: unit -> group type 'a future val task_of: 'a future -> task val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool val ML_statistics: bool Unsynchronized.ref val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: group -> unit val cancel: 'a future -> unit val error_message: Position.T -> (serial * string) * string option -> unit val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool} val default_params: params val forks: params -> (unit -> 'a) list -> 'a future list val fork: (unit -> 'a) -> 'a future val get_finished: 'a future -> 'a val join_results: 'a future list -> 'a Exn.result list val join_result: 'a future -> 'a Exn.result val joins: 'a future list -> 'a list val join: 'a future -> 'a val forked_results: {name: string, deps: Task_Queue.task list} -> (unit -> 'a) list -> 'a Exn.result list val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b val enabled: unit -> bool val relevant: 'a list -> bool val proofs_enabled: int -> bool val proofs_enabled_timing: Time.time -> bool val value_result: 'a Exn.result -> 'a future val value: 'a -> 'a future val cond_forks: params -> (unit -> 'a) list -> 'a future list val map: ('a -> 'b) -> 'a future -> 'b future val promise_name: string -> (unit -> unit) -> 'a future val promise: (unit -> unit) -> 'a future val fulfill_result: 'a future -> 'a Exn.result -> unit val fulfill: 'a future -> 'a -> unit val snapshot: group list -> task list val shutdown: unit -> unit end; structure Future: FUTURE = struct (** future values **) type task = Task_Queue.task; type group = Task_Queue.group; val new_group = Task_Queue.new_group; (* identifiers *) local val worker_task_var = Thread_Data.var () : task Thread_Data.var; in fun worker_task () = Thread_Data.get worker_task_var; fun setmp_worker_task task f x = Thread_Data.setmp worker_task_var (SOME task) f x; end; val worker_group = Option.map Task_Queue.group_of_task o worker_task; fun the_worker_group () = (case worker_group () of SOME group => group | NONE => raise Fail "Missing worker thread context"); fun worker_subgroup () = new_group (worker_group ()); fun worker_joining e = (case worker_task () of NONE => e () | SOME task => Task_Queue.joining task e); fun worker_waiting deps e = (case worker_task () of NONE => e () | SOME task => Task_Queue.waiting task deps e); (* datatype future *) type 'a result = 'a Exn.result Single_Assignment.var; datatype 'a future = Value of 'a Exn.result | Future of {promised: bool, task: task, result: 'a result}; fun task_of (Value _) = Task_Queue.dummy_task | task_of (Future {task, ...}) = task; fun peek (Value res) = SOME res | peek (Future {result, ...}) = Single_Assignment.peek result; fun is_finished x = is_some (peek x); val _ = ML_system_pp (fn depth => fn pretty => fn x => (case peek x of NONE => PolyML.PrettyString "" | SOME (Exn.Exn _) => PolyML.PrettyString "" | SOME (Exn.Res y) => pretty (y, depth))); (** scheduling **) (* synchronization *) val scheduler_event = ConditionVar.conditionVar (); val work_available = ConditionVar.conditionVar (); val work_finished = ConditionVar.conditionVar (); local val lock = Mutex.mutex (); in fun SYNCHRONIZED name = Multithreading.synchronized name lock; fun wait cond = (*requires SYNCHRONIZED*) Multithreading.sync_wait NONE cond lock; fun wait_timeout timeout cond = (*requires SYNCHRONIZED*) Multithreading.sync_wait (SOME (Time.now () + timeout)) cond lock; fun signal cond = (*requires SYNCHRONIZED*) ConditionVar.signal cond; fun broadcast cond = (*requires SYNCHRONIZED*) ConditionVar.broadcast cond; end; (* global state *) val queue = Unsynchronized.ref Task_Queue.empty; val next = Unsynchronized.ref 0; val scheduler = Unsynchronized.ref (NONE: Thread.thread option); val canceled = Unsynchronized.ref ([]: group list); val do_shutdown = Unsynchronized.ref false; val max_workers = Unsynchronized.ref 0; val max_active = Unsynchronized.ref 0; val status_ticks = Unsynchronized.ref 0; val last_round = Unsynchronized.ref Time.zeroTime; val next_round = seconds 0.05; datatype worker_state = Working | Waiting | Sleeping; val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); fun count_workers state = (*requires SYNCHRONIZED*) fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0; (* status *) val ML_statistics = Unsynchronized.ref false; fun report_status () = (*requires SYNCHRONIZED*) if ! ML_statistics then let val {ready, pending, running, passive, urgent, total} = Task_Queue.status (! queue); val workers_total = length (! workers); val workers_active = count_workers Working; val workers_waiting = count_workers Waiting; val stats = [("now", Value.print_real (Time.toReal (Time.now ()))), ("tasks_ready", Value.print_int ready), ("tasks_pending", Value.print_int pending), ("tasks_running", Value.print_int running), ("tasks_passive", Value.print_int passive), ("tasks_urgent", Value.print_int urgent), ("tasks_total", Value.print_int total), ("workers_total", Value.print_int workers_total), ("workers_active", Value.print_int workers_active), ("workers_waiting", Value.print_int workers_waiting)] @ ML_Statistics.get (); in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end else (); (* cancellation primitives *) fun cancel_now group = (*requires SYNCHRONIZED*) let val running = Task_Queue.cancel (! queue) group; val _ = running |> List.app (fn thread => if Isabelle_Thread.is_self thread then () else Isabelle_Thread.interrupt_unsynchronized thread); in running end; fun cancel_all () = (*requires SYNCHRONIZED*) let val (groups, threads) = Task_Queue.cancel_all (! queue); val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads; in groups end; fun cancel_later group = (*requires SYNCHRONIZED*) (Unsynchronized.change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event); fun interruptible_task f x = Thread_Attributes.with_attributes (if is_some (worker_task ()) then Thread_Attributes.private_interrupts else Thread_Attributes.public_interrupts) (fn _ => f x) before Thread_Attributes.expose_interrupt (); (* worker threads *) fun worker_exec (task, jobs) = let val group = Task_Queue.group_of_task task; val valid = not (Task_Queue.is_canceled group); val ok = Task_Queue.running task (fn () => setmp_worker_task task (fn () => fold (fn job => fn ok => job valid andalso ok) jobs true) ()); val _ = if ! Multithreading.trace >= 2 then Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) [] else (); val _ = SYNCHRONIZED "finish" (fn () => let val maximal = Unsynchronized.change_result queue (Task_Queue.finish task); val test = Exn.capture Thread_Attributes.expose_interrupt (); val _ = if ok andalso not (Exn.is_interrupt_exn test) then () else if null (cancel_now group) then () else cancel_later group; val _ = broadcast work_finished; val _ = if maximal then () else signal work_available; in () end); in () end; fun worker_wait worker_state cond = (*requires SYNCHRONIZED*) (case AList.lookup Thread.equal (! workers) (Thread.self ()) of SOME state => Unsynchronized.setmp state worker_state wait cond | NONE => wait cond); fun worker_next () = (*requires SYNCHRONIZED*) if length (! workers) > ! max_workers then (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ())); signal work_available; NONE) else let val urgent_only = count_workers Working > ! max_active in (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of NONE => (worker_wait Sleeping work_available; worker_next ()) | some => (signal work_available; some)) end; fun worker_loop name = (case SYNCHRONIZED name (fn () => worker_next ()) of NONE => () | SOME work => (worker_exec work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) let - val threads_stack_limit = - Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0); - val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit; val worker = - Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false} + Isabelle_Thread.fork + {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false} (fn () => worker_loop name); in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg); (* scheduler *) fun scheduler_next () = (*requires SYNCHRONIZED*) let val now = Time.now (); val tick = ! last_round + next_round <= now; val _ = if tick then last_round := now else (); (* runtime status *) val _ = if tick then Unsynchronized.change status_ticks (fn i => i + 1) else (); val _ = if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 10) = 0 then report_status () else (); val _ = if not tick orelse forall (Thread.isActive o #1) (! workers) then () else let val (alive, dead) = List.partition (Thread.isActive o #1) (! workers); val _ = workers := alive; in Multithreading.tracing 0 (fn () => "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads") end; (* worker pool adjustments *) val max_active0 = ! max_active; val max_workers0 = ! max_workers; val m = if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0 else Multithreading.max_threads (); val _ = max_active := m; val _ = max_workers := 2 * m; val missing = ! max_workers - length (! workers); val _ = if missing > 0 then funpow missing (fn () => ignore (worker_start ("worker " ^ string_of_int (Unsynchronized.inc next)))) () else (); val _ = if ! max_active = max_active0 andalso ! max_workers = max_workers0 then () else signal work_available; (* canceled groups *) val _ = if null (! canceled) then () else (Multithreading.tracing 1 (fn () => string_of_int (length (! canceled)) ^ " canceled groups"); Unsynchronized.change canceled (filter_out (null o cancel_now)); signal work_available); (* delay loop *) val _ = Exn.release (wait_timeout next_round scheduler_event); (* shutdown *) val continue = not (! do_shutdown andalso null (! workers)); val _ = if continue then () else (report_status (); scheduler := NONE); val _ = broadcast scheduler_event; in continue end handle exn => if Exn.is_interrupt exn then (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt"); List.app cancel_later (cancel_all ()); signal work_available; true) else Exn.reraise exn; fun scheduler_loop () = (while Thread_Attributes.with_attributes (Thread_Attributes.sync_interrupts Thread_Attributes.public_interrupts) (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ())) do (); last_round := Time.zeroTime); fun scheduler_active () = (*requires SYNCHRONIZED*) (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); fun scheduler_check () = (*requires SYNCHRONIZED*) (do_shutdown := false; if scheduler_active () then () else scheduler := SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false} scheduler_loop)); (** futures **) (* cancel *) fun cancel_group_unsynchronized group = (*requires SYNCHRONIZED*) let val _ = if null (cancel_now group) then () else cancel_later group; val _ = signal work_available; val _ = scheduler_check (); in () end; fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () => cancel_group_unsynchronized group); fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x)); (* results *) fun error_message pos ((serial, msg), exec_id) = Position.setmp_thread_data pos (fn () => let val id = Position.get_id pos in if is_none id orelse is_none exec_id orelse id = exec_id then Output.error_message' (serial, msg) else () end) (); fun identify_result pos res = res |> Exn.map_exn (fn exn => let val exec_id = (case Position.get_id pos of NONE => [] | SOME id => [(Markup.exec_idN, id)]) in Par_Exn.identify exec_id exn end); fun assign_result group result res = let val _ = Single_Assignment.assign result res handle exn as Fail _ => (case Single_Assignment.peek result of SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn) | _ => Exn.reraise exn); val ok = (case the (Single_Assignment.peek result) of Exn.Exn exn => (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false) | Exn.Res _ => true); in ok end; (* future jobs *) fun future_job group atts (e: unit -> 'a) = let val result = Single_Assignment.var "future" : 'a result; val pos = Position.thread_data (); val context = Context.get_generic_context (); fun job ok = let val res = if ok then Exn.capture (fn () => Thread_Attributes.with_attributes atts (fn _ => (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) () else Exn.interrupt_exn; in assign_result group result (identify_result pos res) end; in (result, job) end; (* fork *) type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}; val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true}; fun forks ({name, group, deps, pri, interrupts}: params) es = if null es then [] else let val grp = (case group of NONE => worker_subgroup () | SOME grp => grp); fun enqueue e queue = let val atts = if interrupts then Thread_Attributes.private_interrupts else Thread_Attributes.no_interrupts; val (result, job) = future_job grp atts e; val (task, queue') = Task_Queue.enqueue name grp deps pri job queue; val future = Future {promised = false, task = task, result = result}; in (future, queue') end; in SYNCHRONIZED "enqueue" (fn () => let val (futures, queue') = fold_map enqueue es (! queue); val _ = queue := queue'; val minimal = forall (not o Task_Queue.known_task queue') deps; val _ = if minimal then signal work_available else (); val _ = scheduler_check (); in futures end) end; fun fork e = (singleton o forks) {name = "fork", group = NONE, deps = [], pri = 0, interrupts = true} e; (* join *) fun get_result x = (case peek x of NONE => Exn.Exn (Fail "Unfinished future") | SOME res => if Exn.is_interrupt_exn res then (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of [] => res | exns => Exn.Exn (Par_Exn.make exns)) else res); fun get_finished x = Exn.release (get_result x); local fun join_next atts deps = (*requires SYNCHRONIZED*) if null deps then NONE else (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of (NONE, []) => NONE | (NONE, deps') => (worker_waiting deps' (fn () => Thread_Attributes.with_attributes atts (fn _ => Exn.release (worker_wait Waiting work_finished))); join_next atts deps') | (SOME work, deps') => SOME (work, deps')); fun join_loop atts deps = (case SYNCHRONIZED "join" (fn () => join_next atts deps) of NONE => () | SOME (work, deps') => (worker_joining (fn () => worker_exec work); join_loop atts deps')); in fun join_results xs = let val _ = if forall is_finished xs then () else if is_some (worker_task ()) then Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => join_loop orig_atts (map task_of xs)) else xs |> List.app (fn Value _ => () | Future {result, ...} => ignore (Single_Assignment.await result)); in map get_result xs end; end; fun join_result x = singleton join_results x; fun joins xs = Par_Exn.release_all (join_results xs); fun join x = Exn.release (join_result x); (* forked results: nested parallel evaluation *) fun forked_results {name, deps} es = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val (group, pri) = (case worker_task () of SOME task => (new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task) | NONE => (new_group NONE, 0)); val futures = forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es; in restore_attributes join_results futures handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn) end) (); (* task context for running thread *) fun task_context name group f x = Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts => let val (result, job) = future_job group orig_atts (fn () => f x); val task = SYNCHRONIZED "enroll" (fn () => Unsynchronized.change_result queue (Task_Queue.enroll (Thread.self ()) name group)); val _ = worker_exec (task, [job]); in (case Single_Assignment.peek result of NONE => raise Fail "Missing task context result" | SOME res => Exn.release res) end); (* scheduling parameters *) fun enabled () = let val threads = Multithreading.max_threads () in threads > 1 andalso let val lim = threads * Options.default_int "parallel_limit" in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end end; val relevant = (fn [] => false | [_] => false | _ => enabled ()); fun proofs_enabled n = ! Multithreading.parallel_proofs >= n andalso is_some (worker_task ()) andalso enabled (); fun proofs_enabled_timing t = proofs_enabled 1 andalso Time.toReal t >= Options.default_real "parallel_subproofs_threshold"; (* fast-path operations -- bypass task queue if possible *) fun value_result (res: 'a Exn.result) = let val task = Task_Queue.dummy_task; val group = Task_Queue.group_of_task task; val result = Single_Assignment.var "value" : 'a result; val _ = assign_result group result (identify_result (Position.thread_data ()) res); in Future {promised = false, task = task, result = result} end; fun value x = value_result (Exn.Res x); fun cond_forks args es = if enabled () then forks args es else map (fn e => value_result (Exn.interruptible_capture e ())) es; fun map_future f x = if is_finished x then value_result (Exn.interruptible_capture (f o join) x) else let val task = task_of x; val group = Task_Queue.group_of_task task; val (result, job) = future_job group Thread_Attributes.private_interrupts (fn () => f (join x)); val extended = SYNCHRONIZED "extend" (fn () => (case Task_Queue.extend task job (! queue) of SOME queue' => (queue := queue'; true) | NONE => false)); in if extended then Future {promised = false, task = task, result = result} else (singleton o cond_forks) {name = "map_future", group = SOME group, deps = [task], pri = Task_Queue.pri_of_task task, interrupts = true} (fn () => f (join x)) end; (* promised futures -- fulfilled by external means *) fun promise_name name abort : 'a future = let val group = worker_subgroup (); val result = Single_Assignment.var "promise" : 'a result; fun assign () = assign_result group result Exn.interrupt_exn handle Fail _ => true | exn => if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise" else Exn.reraise exn; fun job () = Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ => Exn.release (Exn.capture assign () before abort ())); val task = SYNCHRONIZED "enqueue_passive" (fn () => Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job)); in Future {promised = true, task = task, result = result} end; fun promise abort = promise_name "passive" abort; fun fulfill_result (Future {promised = true, task, result}) res = let val group = Task_Queue.group_of_task task; val pos = Position.thread_data (); fun job ok = assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn); val _ = Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ => let val passive_job = SYNCHRONIZED "fulfill_result" (fn () => Unsynchronized.change_result queue (Task_Queue.dequeue_passive (Thread.self ()) task)); in (case passive_job of SOME true => worker_exec (task, [job]) | SOME false => () | NONE => ignore (job (not (Task_Queue.is_canceled group)))) end); val _ = if is_some (Single_Assignment.peek result) then () else worker_waiting [task] (fn () => ignore (Single_Assignment.await result)); in () end | fulfill_result _ _ = raise Fail "Not a promised future"; fun fulfill x res = fulfill_result x (Exn.Res res); (* snapshot: current tasks of groups *) fun snapshot [] = [] | snapshot groups = SYNCHRONIZED "snapshot" (fn () => Task_Queue.group_tasks (! queue) groups); (* shutdown *) fun shutdown () = if is_some (worker_task ()) then raise Fail "Cannot shutdown while running as worker thread" else SYNCHRONIZED "shutdown" (fn () => while scheduler_active () do (do_shutdown := true; Multithreading.tracing 1 (fn () => "SHUTDOWN: wait"); wait scheduler_event)); (*final declarations of this structure!*) val map = map_future; end; type 'a future = 'a Future.future; diff --git a/src/Pure/Concurrent/isabelle_thread.ML b/src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML +++ b/src/Pure/Concurrent/isabelle_thread.ML @@ -1,73 +1,80 @@ (* Title: Pure/Concurrent/isabelle_thread.ML Author: Makarius Isabelle-specific thread management. *) signature ISABELLE_THREAD = sig val is_self: Thread.thread -> bool val get_name: unit -> string + val stack_limit: unit -> int option type params = {name: string, stack_limit: int option, interrupts: bool} val attributes: params -> Thread.threadAttribute list val fork: params -> (unit -> unit) -> Thread.thread val join: Thread.thread -> unit val interrupt_unsynchronized: Thread.thread -> unit end; structure Isabelle_Thread: ISABELLE_THREAD = struct (* self *) fun is_self thread = Thread.equal (Thread.self (), thread); (* unique name *) local val name_var = Thread_Data.var () : string Thread_Data.var; val count = Counter.make (); in fun get_name () = (case Thread_Data.get name_var of SOME name => name | NONE => raise Fail "Isabelle-specific thread required"); fun set_name base = Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ()))); end; (* fork *) +fun stack_limit () = + let + val threads_stack_limit = + Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0); + in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end; + type params = {name: string, stack_limit: int option, interrupts: bool}; fun attributes ({stack_limit, interrupts, ...}: params) = Thread.MaximumMLStack stack_limit :: Thread_Attributes.convert_attributes (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts); fun fork (params: params) body = Thread.fork (fn () => Exn.trace General.exnMessage tracing (fn () => (set_name (#name params); body ()) handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn), attributes params); (* join *) fun join thread = while Thread.isActive thread do OS.Process.sleep (seconds 0.1); (* interrupt *) fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => (); end; diff --git a/src/Pure/General/word.scala b/src/Pure/General/word.scala --- a/src/Pure/General/word.scala +++ b/src/Pure/General/word.scala @@ -1,87 +1,87 @@ /* Title: Pure/General/word.scala Author: Makarius Support for words within Unicode text. */ package isabelle import java.text.Bidi import java.util.Locale object Word { /* directionality */ def bidi_detect(str: String): Boolean = str.exists(c => c >= 0x590) && Bidi.requiresBidi(str.toArray, 0, str.length) def bidi_override(str: String): String = if (bidi_detect(str)) "\u200E\u202D" + str + "\u202C" else str /* case */ def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) def capitalize(str: String): String = if (str.length == 0) str else { val n = Character.charCount(str.codePointAt(0)) uppercase(str.substring(0, n)) + lowercase(str.substring(n)) } def perhaps_capitalize(str: String): String = if (Codepoint.iterator(str).forall(c => Character.isLowerCase(c) || Character.isDigit(c))) capitalize(str) else str sealed abstract class Case case object Lowercase extends Case case object Uppercase extends Case case object Capitalized extends Case object Case { def apply(c: Case, str: String): String = c match { case Lowercase => lowercase(str) case Uppercase => uppercase(str) case Capitalized => capitalize(str) } def unapply(str: String): Option[Case] = if (str.nonEmpty) { if (Codepoint.iterator(str).forall(Character.isLowerCase)) Some(Lowercase) else if (Codepoint.iterator(str).forall(Character.isUpperCase)) Some(Uppercase) else { val it = Codepoint.iterator(str) if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase)) Some(Capitalized) else None } } else None } /* sequence of words */ def implode(words: Iterable[String]): String = words.iterator.mkString(" ") def explode(sep: Char => Boolean, text: String): List[String] = Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList def explode(sep: Char, text: String): List[String] = explode(_ == sep, text) def explode(text: String): List[String] = - explode(Character.isWhitespace(_), text) + explode(Character.isWhitespace _, text) /* brackets */ - val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃" - val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄" + val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪" + val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫" } diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala +++ b/src/Pure/ML/ml_process.scala @@ -1,192 +1,195 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.io.{File => JFile} object ML_Process { def apply(options: Options, sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, eval_main: String = "", args: List[String] = Nil, modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), session_base: Option[Sessions.Base] = None): Bash.Process = { val logic_name = Isabelle_System.default_logic(logic) val heaps: List[String] = if (raw_ml_system) Nil else { sessions_structure.selection(Sessions.Selection.session(logic_name)). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) } val eval_init = if (heaps.isEmpty) { List( """ fun chapter (_: string) = (); fun section (_: string) = (); fun subsection (_: string) = (); fun subsubsection (_: string) = (); fun paragraph (_: string) = (); fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, if (Platform.is_windows) "fun exit 0 = OS.Process.exit OS.Process.success" + " | exit 1 = OS.Process.exit OS.Process.failure" + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", "PolyML.Compiler.prompt1 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } else List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + ML_Syntax.print_string_bytes(": " + logic_name + "\n") + "); OS.Process.exit OS.Process.failure)") val eval_modes = if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) // options val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base val eval_session_base = session_base match { case None => Nil case Some(base) => def print_table(table: List[(String, String)]): String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) def print_list(list: List[String]): String = ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) def print_sessions(list: List[(String, Position.T)]): String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) - List("Resources.init_session_base" + - " {session_positions = " + print_sessions(sessions_structure.session_positions) + + List("Resources.init_session" + + "{pide = false" + + ", session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") } // process val eval_process = proper_string(eval_main).getOrElse( if (heaps.isEmpty) { "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) } else "Isabelle_Process.init ()") // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) + val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) + val ml_runtime_options = { val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) val ml_options1 = if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options else ml_options ::: List("--gcthreads", options.int("threads").toString) val ml_options2 = if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 else ml_options1 ::: List("--codepage", "utf8") ml_options2 } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, - env = env ++ env_options ++ env_tmp, + env = env ++ env_options ++ env_tmp ++ env_functions, redirect = redirect, cleanup = () => { isabelle_process_options.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => { var dirs: List[Path] = Nil var eval_args: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var options = Options.init() val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode. """, "T:" -> (arg => eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg)) val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) val rc = ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) .result().print_stdout.rc sys.exit(rc) }) } diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML +++ b/src/Pure/PIDE/markup.ML @@ -1,794 +1,796 @@ (* Title: Pure/PIDE/markup.ML Author: Makarius Quasi-abstract markup elements. *) signature MARKUP = sig type T = string * Properties.T val empty: T val is_empty: T -> bool val properties: Properties.T -> T -> T val nameN: string val name: string -> T -> T val xnameN: string val xname: string -> T -> T val kindN: string val serialN: string val serial_properties: int -> Properties.T val instanceN: string val meta_titleN: string val meta_title: T val meta_creatorN: string val meta_creator: T val meta_contributorN: string val meta_contributor: T val meta_dateN: string val meta_date: T val meta_licenseN: string val meta_license: T val meta_descriptionN: string val meta_description: T val languageN: string val symbolsN: string val delimitedN: string val is_delimited: Properties.T -> bool val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_Isar: bool -> T val language_method: T val language_attribute: T val language_sort: bool -> T val language_type: bool -> T val language_term: bool -> T val language_prop: bool -> T val language_ML: bool -> T val language_SML: bool -> T val language_document: bool -> T val language_document_marker: T val language_antiquotation: T val language_text: bool -> T val language_verbatim: bool -> T val language_latex: bool -> T val language_rail: T val language_path: T val language_mixfix: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val defN: string val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string val end_offsetN: string val fileN: string val idN: string val position_properties': string list val position_properties: string list val positionN: string val position: T val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T val export_pathN: string val export_path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T + val scala_functionN: string val scala_function: string -> T val markupN: string val consistentN: string val unbreakableN: string val block_properties: string list val indentN: string val widthN: string val blockN: string val block: bool -> int -> T val breakN: string val break: int -> int -> T val fbreakN: string val fbreak: T val itemN: string val item: T val wordsN: string val words: T val hiddenN: string val hidden: T val deleteN: string val delete: T val system_optionN: string val sessionN: string val theoryN: string val classN: string val type_nameN: string val constantN: string val fixedN: string val fixed: string -> T val caseN: string val case_: string -> T val dynamic_factN: string val dynamic_fact: string -> T val literal_factN: string val literal_fact: string -> T val method_modifierN: string val tfreeN: string val tfree: T val tvarN: string val tvar: T val freeN: string val free: T val skolemN: string val skolem: T val boundN: string val bound: T val varN: string val var: T val numeralN: string val numeral: T val literalN: string val literal: T val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T val inner_cartoucheN: string val inner_cartouche: T val token_rangeN: string val token_range: T val sortingN: string val sorting: T val typingN: string val typing: T val class_parameterN: string val class_parameter: T val ML_keyword1N: string val ML_keyword1: T val ML_keyword2N: string val ML_keyword2: T val ML_keyword3N: string val ML_keyword3: T val ML_delimiterN: string val ML_delimiter: T val ML_tvarN: string val ML_tvar: T val ML_numeralN: string val ML_numeral: T val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T val ML_commentN: string val ML_comment: T val ML_defN: string val ML_openN: string val ML_structureN: string val ML_typingN: string val ML_typing: T val ML_breakpointN: string val ML_breakpoint: int -> T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val file_typeN: string val antiquotationN: string val ML_antiquotationN: string val document_antiquotationN: string val document_antiquotation_optionN: string val raw_textN: string val raw_text: T val plain_textN: string val plain_text: T val paragraphN: string val paragraph: T val text_foldN: string val text_fold: T val document_markerN: string val document_marker: T val document_tagN: string val document_tag: string -> T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T val markdown_listN: string val markdown_list: string -> T val itemizeN: string val enumerateN: string val descriptionN: string val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command_properties: T -> T val keywordN: string val keyword_properties: T -> T val stringN: string val string: T val alt_stringN: string val alt_string: T val verbatimN: string val verbatim: T val cartoucheN: string val cartouche: T val commentN: string val comment: T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T val keyword3N: string val keyword3: T val quasi_keywordN: string val quasi_keyword: T val improperN: string val improper: T val operatorN: string val operator: T val comment1N: string val comment1: T val comment2N: string val comment2: T val comment3N: string val comment3: T val elapsedN: string val cpuN: string val gcN: string val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} val command_timingN: string val command_timing_properties: {file: string, offset: int, name: string} -> Time.time -> Properties.T val parse_command_timing_properties: Properties.T -> ({file: string, offset: int, name: string} * Time.time) option val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T val command_indentN: string val command_indent: int -> T val goalN: string val goal: T val subgoalN: string val subgoal: string -> T val taskN: string val forkedN: string val forked: T val joinedN: string val joined: T val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T val canceledN: string val canceled: T val initializedN: string val initialized: T val finalizedN: string val finalized: T val consolidatingN: string val consolidating: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string val statusN: string val status: T val resultN: string val result: T val writelnN: string val writeln: T val stateN: string val state: T val informationN: string val information: T val tracingN: string val tracing: T val warningN: string val warning: T val legacyN: string val legacy: T val errorN: string val error: T val systemN: string val system: T val protocolN: string val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: unit -> T val intensifyN: string val intensify: T val browserN: string val graphviewN: string val theory_exportsN: string val sendbackN: string val paddingN: string val padding_line: Properties.entry val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string val functionN: string val commands_accepted: Properties.T val assign_update: Properties.T val removed_versions: Properties.T val protocol_handler: string -> Properties.T val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T val ML_statistics: Properties.entry val task_statistics: Properties.entry val command_timing: Properties.entry val theory_timing: Properties.entry val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T val exportN: string type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool} val export: export_args -> Properties.T val debugger_state: string -> Properties.T val debugger_output: string -> Properties.T val simp_trace_panelN: string val simp_trace_logN: string val simp_trace_stepN: string val simp_trace_recurseN: string val simp_trace_hintN: string val simp_trace_ignoreN: string val simp_trace_cancel: serial -> Properties.T type output = Output.output * Output.output val no_output: output val add_mode: string -> (T -> output) -> unit val output: T -> output val enclose: T -> Output.output -> Output.output val markup: T -> string -> string val markups: T list -> string -> string val markup_only: T -> string val markup_report: string -> string end; structure Markup: MARKUP = struct (** markup elements **) (* basic markup *) type T = string * Properties.T; val empty = ("", []); fun is_empty ("", _) = true | is_empty _ = false; fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); fun markup_elem name = (name, (name, []): T); fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); (* misc properties *) val nameN = "name"; fun name a = properties [(nameN, a)]; val xnameN = "xname"; fun xname a = properties [(xnameN, a)]; val kindN = "kind"; val serialN = "serial"; fun serial_properties i = [(serialN, Value.print_int i)]; val instanceN = "instance"; (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *) val (meta_titleN, meta_title) = markup_elem "meta_title"; val (meta_creatorN, meta_creator) = markup_elem "meta_creator"; val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor"; val (meta_dateN, meta_date) = markup_elem "meta_date"; val (meta_licenseN, meta_license) = markup_elem "meta_license"; val (meta_descriptionN, meta_description) = markup_elem "meta_description"; (* embedded languages *) val languageN = "language"; val symbolsN = "symbols"; val antiquotesN = "antiquotes"; val delimitedN = "delimited" fun is_delimited props = Properties.get props delimitedN = SOME "true"; fun language {name, symbols, antiquotes, delimited} = (languageN, [(nameN, name), (symbolsN, Value.print_bool symbols), (antiquotesN, Value.print_bool antiquotes), (delimitedN, Value.print_bool delimited)]); fun language' {name, symbols, antiquotes} delimited = language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; val language_method = language {name = "method", symbols = true, antiquotes = false, delimited = false}; val language_attribute = language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; val language_type = language' {name = "type", symbols = true, antiquotes = false}; val language_term = language' {name = "term", symbols = true, antiquotes = false}; val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; val language_document = language' {name = "document", symbols = false, antiquotes = true}; val language_document_marker = language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true}; val language_mixfix = language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; (* formal entities *) val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; fun entity kind name = (entityN, (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); val defN = "def"; val refN = "ref"; (* completion *) val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; val (updateN, update) = markup_elem "update"; (* position *) val lineN = "line"; val end_lineN = "end_line"; val offsetN = "offset"; val end_offsetN = "end_offset"; val fileN = "file"; val idN = "id"; val position_properties' = [fileN, idN]; val position_properties = [lineN, offsetN, end_offsetN] @ position_properties'; val (positionN, position) = markup_elem "position"; (* expression *) val expressionN = "expression"; fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); (* citation *) val (citationN, citation) = markup_string "citation" nameN; (* external resources *) val (pathN, path) = markup_string "path" nameN; val (export_pathN, export_path) = markup_string "export_path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; +val (scala_functionN, scala_function) = markup_string "scala_function" nameN; (* pretty printing *) val markupN = "markup"; val consistentN = "consistent"; val unbreakableN = "unbreakable"; val indentN = "indent"; val block_properties = [markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; val blockN = "block"; fun block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val breakN = "break"; fun break w i = (breakN, (if w <> 0 then [(widthN, Value.print_int w)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val (fbreakN, fbreak) = markup_elem "fbreak"; val (itemN, item) = markup_elem "item"; (* text properties *) val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; val (deleteN, delete) = markup_elem "delete"; (* misc entities *) val system_optionN = "system_option"; val sessionN = "session"; val theoryN = "theory"; val classN = "class"; val type_nameN = "type_name"; val constantN = "constant"; val (fixedN, fixed) = markup_string "fixed" nameN; val (caseN, case_) = markup_string "case" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; val method_modifierN = "method_modifier"; (* inner syntax *) val (tfreeN, tfree) = markup_elem "tfree"; val (tvarN, tvar) = markup_elem "tvar"; val (freeN, free) = markup_elem "free"; val (skolemN, skolem) = markup_elem "skolem"; val (boundN, bound) = markup_elem "bound"; val (varN, var) = markup_elem "var"; val (numeralN, numeral) = markup_elem "numeral"; val (literalN, literal) = markup_elem "literal"; val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; val (token_rangeN, token_range) = markup_elem "token_range"; val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; val (class_parameterN, class_parameter) = markup_elem "class_parameter"; (* ML *) val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; val ML_defN = "ML_def"; val ML_openN = "ML_open"; val ML_structureN = "ML_structure"; val (ML_typingN, ML_typing) = markup_elem "ML_typing"; val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; (* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; val file_typeN = "file_type"; val antiquotationN = "antiquotation"; val ML_antiquotationN = "ML_antiquotation"; val document_antiquotationN = "document_antiquotation"; val document_antiquotation_optionN = "document_antiquotation_option"; (* document text *) val (raw_textN, raw_text) = markup_elem "raw_text"; val (plain_textN, plain_text) = markup_elem "plain_text"; val (paragraphN, paragraph) = markup_elem "paragraph"; val (text_foldN, text_fold) = markup_elem "text_fold"; val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; (* Markdown document structure *) val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; val itemizeN = "itemize"; val enumerateN = "enumerate"; val descriptionN = "description"; (* formal input *) val inputN = "input"; fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); (* outer syntax *) val (command_keywordN, command_keyword) = markup_elem "command_keyword"; val commandN = "command"; val command_properties = properties [(kindN, commandN)]; val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; val (keyword1N, keyword1) = markup_elem "keyword1"; val (keyword2N, keyword2) = markup_elem "keyword2"; val (keyword3N, keyword3) = markup_elem "keyword3"; val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; val (improperN, improper) = markup_elem "improper"; val (operatorN, operator) = markup_elem "operator"; val (stringN, string) = markup_elem "string"; val (alt_stringN, alt_string) = markup_elem "alt_string"; val (verbatimN, verbatim) = markup_elem "verbatim"; val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; (* comments *) val (comment1N, comment1) = markup_elem "comment1"; val (comment2N, comment2) = markup_elem "comment2"; val (comment3N, comment3) = markup_elem "comment3"; (* timing *) val elapsedN = "elapsed"; val cpuN = "cpu"; val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = [(elapsedN, Value.print_time elapsed), (cpuN, Value.print_time cpu), (gcN, Value.print_time gc)]; fun parse_timing_properties props = {elapsed = Properties.seconds props elapsedN, cpu = Properties.seconds props cpuN, gc = Properties.seconds props gcN}; val timingN = "timing"; fun timing t = (timingN, timing_properties t); (* command timing *) val command_timingN = "command_timing"; fun command_timing_properties {file, offset, name} elapsed = [(fileN, file), (offsetN, Value.print_int offset), (nameN, name), (elapsedN, Value.print_time elapsed)]; fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => SOME ({file = file, offset = Value.parse_int offset, name = name}, Properties.seconds props elapsedN) | _ => NONE); (* indentation *) val (command_indentN, command_indent) = markup_int "command_indent" indentN; (* goals *) val (goalN, goal) = markup_elem "goal"; val (subgoalN, subgoal) = markup_string "subgoal" nameN; (* command status *) val taskN = "task"; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; val (finalizedN, finalized) = markup_elem "finalized"; val (consolidatingN, consolidating) = markup_elem "consolidating"; val (consolidatedN, consolidated) = markup_elem "consolidated"; (* messages *) val exec_idN = "exec_id"; val initN = "init"; val (statusN, status) = markup_elem "status"; val (resultN, result) = markup_elem "result"; val (writelnN, writeln) = markup_elem "writeln"; val (stateN, state) = markup_elem "state" val (informationN, information) = markup_elem "information"; val (tracingN, tracing) = markup_elem "tracing"; val (warningN, warning) = markup_elem "warning"; val (legacyN, legacy) = markup_elem "legacy"; val (errorN, error) = markup_elem "error"; val (systemN, system) = markup_elem "system"; val protocolN = "protocol"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; val badN = "bad"; fun bad () = (badN, serial_properties (serial ())); val (intensifyN, intensify) = markup_elem "intensify"; (* active areas *) val browserN = "browser" val graphviewN = "graphview"; val theory_exportsN = "theory_exports"; val sendbackN = "sendback"; val paddingN = "padding"; val padding_line = (paddingN, "line"); val padding_command = (paddingN, "command"); val dialogN = "dialog"; fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); val jedit_actionN = "jedit_action"; (* protocol message functions *) val functionN = "function" val commands_accepted = [(functionN, "commands_accepted")]; val assign_update = [(functionN, "assign_update")]; val removed_versions = [(functionN, "removed_versions")]; fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)]; fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; val ML_statistics = (functionN, "ML_statistics"); val task_statistics = (functionN, "task_statistics"); val command_timing = (functionN, "command_timing"); val theory_timing = (functionN, "theory_timing"); fun loading_theory name = [("function", "loading_theory"), ("name", name)]; fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name | dest_loading_theory _ = NONE; val build_session_finished = [("function", "build_session_finished")]; val print_operationsN = "print_operations"; val print_operations = [(functionN, print_operationsN)]; (* export *) val exportN = "export"; type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), (nameN, name), ("executable", Value.print_bool executable), ("compress", Value.print_bool compress), ("strict", Value.print_bool strict)]; (* debugger *) fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; (* simplifier trace *) val simp_trace_panelN = "simp_trace_panel"; val simp_trace_logN = "simp_trace_log"; val simp_trace_stepN = "simp_trace_step"; val simp_trace_recurseN = "simp_trace_recurse"; val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; (** print mode operations **) type output = Output.output * Output.output; val no_output = ("", ""); local val default = {output = Output_Primitives.markup_fn}; val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); in fun add_mode name output = Synchronized.change modes (fn tab => (if not (Symtab.defined tab name) then () else Output.warning ("Redefining markup mode " ^ quote name); Symtab.update (name, {output = output}) tab)); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output m = if is_empty m then no_output else #output (get_mode ()) m; val enclose = output #-> Library.enclose; fun markup m = let val (bg, en) = output m in Library.enclose (Output.escape bg) (Output.escape en) end; val markups = fold_rev markup; fun markup_only m = markup m ""; fun markup_report "" = "" | markup_report txt = markup report txt; end; diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,175 +1,180 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Isabelle_Process.protocol_command "Prover.echo" (fn args => List.app writeln args); val _ = + Isabelle_Process.protocol_command "Prover.stop" + (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc)); + +val _ = Isabelle_Process.protocol_command "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = - Isabelle_Process.protocol_command "Prover.init_session_base" + Isabelle_Process.protocol_command "Prover.init_session" (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] => let val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; val decode_list = YXML.parse_body #> let open XML.Decode in list string end; val decode_sessions = YXML.parse_body #> let open XML.Decode in list (pair string properties) end; in - Resources.init_session_base - {session_positions = decode_sessions session_positions_yxml, + Resources.init_session + {pide = true, + session_positions = decode_sessions session_positions_yxml, session_directories = decode_table session_directories_yxml, docs = decode_list doc_names_yxml, global_theories = decode_table global_theories_yxml, loaded_theories = decode_list loaded_theories_yxml} end); val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name blobs_xml toks_xml sources : Document.command = let open XML.Decode; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; in pair (list (variant [fn ([], a) => Exn.Res (pair string (option string) a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; val _ = Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Isabelle_Process.protocol_command "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (blobs_xml, (toks_xml, sources)))) = pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); in decode_command id name blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Isabelle_Process.protocol_command "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) (pair (list (pair string (pair (pair string (list string)) (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update ((new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); in triple int (list string) (list encode_upd) end); in Document.start_execution state' end))); val _ = Isabelle_Process.protocol_command "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)]; in state1 end)); val _ = Isabelle_Process.protocol_command "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Isabelle_Process.protocol_command "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/protocol.scala b/src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala +++ b/src/Pure/PIDE/protocol.scala @@ -1,464 +1,464 @@ /* Title: Pure/PIDE/protocol.scala Author: Makarius Protocol message formats for interactive proof documents. */ package isabelle object Protocol { /* markers for inlined messages */ val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") val Export_Marker = Protocol_Message.Marker("export") val Meta_Info_Marker = Protocol_Message.Marker("meta_info") val Timing_Marker = Protocol_Message.Marker("Timing") val Command_Timing_Marker = Protocol_Message.Marker("command_timing") val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") val Error_Message_Marker = Protocol_Message.Marker("error_message") /* document editing */ object Commands_Accepted { def unapply(text: String): Option[List[Document_ID.Command]] = try { Some(space_explode(',', text).map(Value.Long.parse)) } catch { case ERROR(_) => None } val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) } object Assign_Update { def unapply(text: String) : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = { try { import XML.Decode._ def decode_upd(body: XML.Body): (Long, List[Long]) = space_explode(',', string(body)).map(Value.Long.parse) match { case a :: bs => (a, bs) case _ => throw new XML.XML_Body(body) } Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } } object Removed { def unapply(text: String): Option[List[Document_ID.Version]] = try { import XML.Decode._ Some(list(long)(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } /* command timing */ object Command_Timing { def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] = props match { case Markup.Command_Timing(args) => (args, args) match { case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing)) case _ => None } case _ => None } } /* theory timing */ object Theory_Timing { def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = props match { case Markup.Theory_Timing(args) => (args, args) match { case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) case _ => None } case _ => None } } /* result messages */ def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean = body match { case List(elem: XML.Elem) => pred(elem) case _ => false } def is_result(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.RESULT, _), _) => true case _ => false } def is_tracing(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.TRACING, _), _) => true case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true case _ => false } def is_state(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.STATE, _), _) => true case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true case _ => false } def is_information(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.INFORMATION, _), _) => true case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true case _ => false } def is_writeln(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WRITELN, _), _) => true case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true case _ => false } def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true case _ => false } def is_legacy(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.LEGACY, _), _) => true case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true case _ => false } def is_error(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.ERROR, _), _) => true case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true case _ => false } def is_inlined(msg: XML.Tree): Boolean = !(is_result(msg) || is_tracing(msg) || is_state(msg)) def is_exported(msg: XML.Tree): Boolean = is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) def message_text(body: XML.Body, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Pretty.Default_Metric): String = { val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin, breakgain = breakgain, metric = metric) if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) else if (is_message(is_error, body)) Output.error_prefix(text) else text } /* export */ object Export { sealed case class Args( id: Option[String], serial: Long, theory_name: String, name: String, executable: Boolean, compress: Boolean, strict: Boolean) { def compound_name: String = isabelle.Export.compound_name(theory_name, name) } object Marker { def unapply(line: String): Option[(Args, Path)] = line match { case Export_Marker(text) => val props = XML.Decode.properties(YXML.parse_body(text)) props match { case List( (Markup.SERIAL, Value.Long(serial)), (Markup.THEORY_NAME, theory_name), (Markup.NAME, name), (Markup.EXECUTABLE, Value.Boolean(executable)), (Markup.COMPRESS, Value.Boolean(compress)), (Markup.STRICT, Value.Boolean(strict)), (Markup.FILE, file)) if isabelle.Path.is_valid(file) => val args = Args(None, serial, theory_name, name, executable, compress, strict) Some((args, isabelle.Path.explode(file))) case _ => None } case _ => None } } def unapply(props: Properties.T): Option[Args] = props match { case List( (Markup.FUNCTION, Markup.EXPORT), (Markup.ID, id), (Markup.SERIAL, Value.Long(serial)), (Markup.THEORY_NAME, theory_name), (Markup.NAME, name), (Markup.EXECUTABLE, Value.Boolean(executable)), (Markup.COMPRESS, Value.Boolean(compress)), (Markup.STRICT, Value.Boolean(strict))) => Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) case _ => None } } /* breakpoints */ object ML_Breakpoint { def unapply(tree: XML.Tree): Option[Long] = tree match { case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) case _ => None } } /* dialogs */ object Dialog_Args { def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = (props, props, props) match { case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => Some((id, serial, result)) case _ => None } } object Dialog { def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = tree match { case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => Some((id, serial, result)) case _ => None } } object Dialog_Result { def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = { val props = Position.Id(id) ::: Markup.Serial(serial) XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) } def unapply(tree: XML.Tree): Option[String] = tree match { case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) case _ => None } } } trait Protocol { /* protocol commands */ def protocol_command_raw(name: String, args: List[Bytes]): Unit def protocol_command_args(name: String, args: List[String]) def protocol_command(name: String, args: String*): Unit /* options */ def options(opts: Options): Unit = protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) /* session base */ private def encode_table(table: List[(String, String)]): String = { import XML.Encode._ Symbol.encode_yxml(list(pair(string, string))(table)) } private def encode_list(lst: List[String]): String = { import XML.Encode._ Symbol.encode_yxml(list(string)(lst)) } private def encode_sessions(lst: List[(String, Position.T)]): String = { import XML.Encode._ Symbol.encode_yxml(list(pair(string, properties))(lst)) } - def session_base(resources: Resources) + def init_session(resources: Resources) { - protocol_command("Prover.init_session_base", + protocol_command("Prover.init_session", encode_sessions(resources.sessions_structure.session_positions), encode_table(resources.sessions_structure.dest_session_directories), encode_list(resources.session_base.doc_names), encode_table(resources.session_base.global_theories.toList), encode_list(resources.session_base.loaded_theories.keys)) } /* interned items */ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) private def encode_command(command: Command): (String, String, String, String, List[String]) = { import XML.Encode._ val blobs_yxml = { val encode_blob: T[Command.Blob] = variant(List( { case Exn.Res((a, b)) => (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } val toks_yxml = { val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) Symbol.encode_yxml(list(encode_tok)(command.span.content)) } val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources) } def define_command(command: Command) { val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) protocol_command_args( "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources) } def define_commands(commands: List[Command]) { protocol_command_args("Document.define_commands", commands.map(command => { import XML.Encode._ val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) val body = pair(string, pair(string, pair(string, pair(string, list(string)))))( command_id, (name, (blobs_yxml, (toks_yxml, toks_sources)))) YXML.string_of_body(body) })) } def define_commands_bulk(commands: List[Command]) { val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) irregular.foreach(define_command) regular match { case Nil => case List(command) => define_command(command) case _ => define_commands(regular) } } /* execution */ def discontinue_execution(): Unit = protocol_command("Document.discontinue_execution") def cancel_exec(id: Document_ID.Exec): Unit = protocol_command("Document.cancel_exec", Document_ID(id)) /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) { val consolidate_yxml = { import XML.Encode._ Symbol.encode_yxml(list(string)(consolidate.map(_.node))) } val edits_yxml = { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) def encode_edit(name: Document.Node.Name) : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = variant(List( { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => val master_dir = File.standard_url(name.master_dir) val imports = header.imports.map(_.node) val keywords = header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) (Nil, pair(string, pair(string, pair(list(string), pair(list(pair(string, pair(pair(string, list(string)), list(string)))), list(string)))))( (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), list(pair(id, pair(string, list(string))))(c.dest)) })) edits.map({ case (name, edit) => Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) }) } protocol_command_args("Document.update", Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml) } def remove_versions(versions: List[Document.Version]) { val versions_yxml = { import XML.Encode._ Symbol.encode_yxml(list(long)(versions.map(_.id))) } protocol_command("Document.remove_versions", versions_yxml) } /* dialog via document content */ def dialog_result(serial: Long, result: String): Unit = protocol_command("Document.dialog_result", Value.Long(serial), result) } diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,320 +1,327 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string - val init_session_base: - {session_positions: (string * Properties.T) list, + val init_session: + {pide: bool, + session_positions: (string * Properties.T) list, session_directories: (string * string) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val finish_session_base: unit -> unit + val is_pide: unit -> bool val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: string -> (theory -> Token.file list) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T end; structure Resources: RESOURCES = struct (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = - {session_positions = []: (string * entry) list, + {pide = false, + session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; val global_session_base = Synchronized.var "Sessions.base" empty_session_base; -fun init_session_base - {session_positions, session_directories, docs, global_theories, loaded_theories} = +fun init_session + {pide, session_positions, session_directories, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {pide = pide, + session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {session_positions = [], + {pide = false, + session_positions = [], session_directories = Symtab.empty, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); fun get_session_base f = f (Synchronized.value global_session_base); +fun is_pide () = get_session_base #pide; + fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; fun check_name which kind markup ctxt (name, pos) = let val entries = get_session_base which in (case AList.lookup (op =) entries name of SOME entry => (Context_Position.report ctxt pos (markup name entry); name) | NONE => let val completion_report = Completion.make_report (name, pos) (fn completed => entries |> map #1 |> filter completed |> sort_strings |> map (fn a => (a, (kind, a)))); in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end) end; fun markup_session name {pos, serial} = Markup.properties (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name); val check_session = check_name #session_positions "session" markup_session; val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun extend _ = empty; fun merge _ = empty; ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.smart_implode master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base #session_directories) session; in dirs |> get_first (fn dir => let val path = Path.append dir thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files cmd = Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of [] => let val keywords = Thy_Header.get_keywords thy; val master_dir = master_directory thy; val pos = Token.pos_of tok; val src_paths = Keyword.command_files keywords cmd (Path.explode name); in map (Command.read_file master_dir pos) src_paths end | files => map Exn.release files)); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files cmd = parse_files cmd >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir (name, pos) = let fun err msg = error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos Markup.language_path; val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = Path.append dir (Path.explode name) handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); val _ = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => let val _ = check ctxt NONE (name, pos); val latex = space_explode "/" name |> map Latex.output_ascii |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}"); in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end); fun ML_antiq check = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); in val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_verbatim_embedded \<^binding>\doc\ (Scan.lift Parse.embedded_position) check_doc #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,748 +1,748 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]) { consumers.change(Library.update(c)) } def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) } def post(a: A) { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ private[Session] class Syslog(limit: Int) { private var queue = Queue.empty[XML.Elem] private var length = 0 def += (msg: XML.Elem): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } def content: String = synchronized { cat_lines(queue.iterator.map(XML.content)) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } } /* protocol handlers */ abstract class Protocol_Handler { def init(session: Session): Unit = {} def exit(): Unit = {} val functions: List[(String, Prover.Protocol_Output => Boolean)] } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => val xml_cache: XML.Cache = XML.make_cache() val xz_cache: XZ.Cache = XZ.make_cache() /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread) body } def require_dispatcher[A](body: => A): A = { require(dispatcher.check_thread) body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send_wait(() => body) } /* outlets */ val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown() { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit() { delay.revoke() state.change(_ => None) } def update(new_nodes: Set[Document.Node.Name] = Set.empty) { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover) { variable.change(_ => Some(p)) } def reset { variable.change(_ => None) } def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) } } /* file formats */ lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) /* protocol handlers */ private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler(name: String): Option[Session.Protocol_Handler] = protocol_handlers.get(name) def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def init_protocol_handler(name: String): Unit = protocol_handlers.init(name) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil) //{{{ { require(prover.defined) if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) } //}}} /* resulting changes */ def handle_change(change: Session.Change) //{{{ { require(prover.defined) // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command) { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList) } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) } //}}} /* prover output */ def handle_output(output: Prover.Output) //{{{ { def bad_output() { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)) { try { val st = global_state.change_result(f) change_buffer.invoke(false, Nil, List(st.command)) } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Markup.Protocol_Handler(name) if prover.defined => init_protocol_handler(name) case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.ML_Statistics(props) => runtime_statistics.post(Session.Runtime_Statistics(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val export = Export.make_entry("", args, msg.bytes, cache = xz_cache) change_command(_.add_export(id, (args.serial, export))) case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache))) case _ => bad_output() } case List(Markup.Assign_Update.PROPERTY) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.PROPERTY) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, xml_cache)) case _ if output.is_init => prover.get.options(file_formats.prover_options(session_options)) - prover.get.session_base(resources) + prover.get.init_session(resources) phase = Session.Ready debugger.ready() case Markup.Process_Result(result) if output.is_exit => file_formats.stop_session phase = Session.Terminated(result) prover.reset case _ => raw_output_messages.post(output) } } } //}}} /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { syslog += output.message syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { protocol_handlers.exit() global_state.change(_ => Document.State.init) prover.get.terminate } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(file_formats.prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) case Protocol_Command(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover) { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } def protocol_command(name: String, args: String*) { manager.send(Protocol_Command(name, args.toList)) } def cancel_exec(exec_id: Document_ID.Exec) { manager.send(Cancel_Exec(exec_id)) } def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } def update_options(options: Options) { manager.send_wait(Update_Options(options)) } def dialog_result(id: Document_ID.Generic, serial: Long, result: String) { manager.send(Session.Dialog_Result(id, serial, result)) } } diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,356 +1,357 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash_syntax.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "ML/ml_statistics.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala.ML"; +ML_file "System/scala_check.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,262 +1,259 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool - exception STOP - exception EXIT of int + exception STOP of int val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit val init_build: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; val protocol_modes2 = [isabelle_processN, Pretty.symbolicN]; (* protocol commands *) -exception STOP; -exception EXIT of int; +exception STOP of int; -val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false; +val is_protocol_exn = fn STOP _ => true | _ => false; local val commands = Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); in fun protocol_command name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); fun run_command name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle exn => if is_protocol_exn exn then Exn.reraise exn else error ("Isabelle protocol command failure: " ^ quote name))); end; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); (* init protocol -- uninterruptible *) val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); local fun recover crash = (Synchronized.change crashes (cons crash); Output.physical_stderr "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); in fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => let val _ = SHA1.test_samples () handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); val _ = Output.physical_stderr Symbol.STX; (* streams *) val (in_stream, out_stream) = Socket_IO.open_streams address; val _ = Byte_Message.write_line out_stream password; val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); (* messages *) val msg_channel = Message_Channel.make out_stream; fun message name props body = Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name ss = if forall (fn s => s = "") ss then () else let val props' = (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' (XML.blob ss) end; fun report_message ss = if Context_Position.pide_reports () then standard_message [] Markup.reportN ss else (); val serial_props = Markup.serial_properties o serial; val message_context = Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #> Unsynchronized.setmp Private_Output.report_fn report_message #> Unsynchronized.setmp Private_Output.result_fn (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #> Unsynchronized.setmp Private_Output.writeln_fn (fn s => standard_message (serial_props ()) Markup.writelnN s) #> Unsynchronized.setmp Private_Output.state_fn (fn s => standard_message (serial_props ()) Markup.stateN s) #> Unsynchronized.setmp Private_Output.information_fn (fn s => standard_message (serial_props ()) Markup.informationN s) #> Unsynchronized.setmp Private_Output.tracing_fn (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #> Unsynchronized.setmp Private_Output.warning_fn (fn s => standard_message (serial_props ()) Markup.warningN s) #> Unsynchronized.setmp Private_Output.legacy_fn (fn s => standard_message (serial_props ()) Markup.legacyN s) #> Unsynchronized.setmp Private_Output.error_message_fn (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #> Unsynchronized.setmp Private_Output.system_message_fn (fn ss => message Markup.systemN [] (XML.blob ss)) #> Unsynchronized.setmp Private_Output.protocol_message_fn (fn props => fn body => message Markup.protocolN props body) #> Unsynchronized.setmp print_mode ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes)); (* protocol *) fun protocol_loop () = let val _ = (case Byte_Message.read_message in_stream of - NONE => raise STOP + NONE => raise STOP 0 | SOME [] => Output.system_message "Isabelle process: no input" | SOME (name :: args) => run_command name args) handle exn => if is_protocol_exn exn then Exn.reraise exn else (Runtime.exn_system_message exn handle crash => recover crash); in protocol_loop () end; fun protocol () = (Session.init_protocol_handlers (); message Markup.initN [] [XML.Text (Session.welcome ())]; protocol_loop ()); val result = Exn.capture (message_context protocol) (); (* shutdown *) val _ = Future.shutdown (); val _ = Execution.reset (); val _ = Message_Channel.shutdown msg_channel; val _ = BinIO.closeIn in_stream; val _ = BinIO.closeOut out_stream; in (case result of - Exn.Exn STOP => () - | Exn.Exn (EXIT rc) => exit rc + Exn.Exn (STOP rc) => if rc = 0 then () else exit rc | _ => Exn.release result) end); end; (* init options *) fun init_options () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Future.ML_statistics := Options.default_bool "ML_statistics"; Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); Printer.show_markup_default := true); (* generic init *) fun init_modes modes = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol modes (address, password) else init_options () end; fun init () = init_modes (protocol_modes1, protocol_modes2); fun init_build () = init_modes ([], protocol_modes2); end; diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,407 +1,410 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import scala.collection.mutable object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Service]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Service] = { if (_services.isEmpty) init() // unsynchronized check _services.get } - def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized + def init(isabelle_root: String = "", cygwin_root: String = "") { - if (_settings.isEmpty || _services.isEmpty) { - val isabelle_root1 = - bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") - - val cygwin_root1 = - if (Platform.is_windows) - bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") - else "" - - if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) - - def set_cygwin_root() - { - if (Platform.is_windows) - _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) - } - - set_cygwin_root() - - def default(env: Map[String, String], entry: (String, String)): Map[String, String] = - if (env.isDefinedAt(entry._1) || entry._2 == "") env - else env + entry - - val env = - { - val temp_windows = - { - val temp = if (Platform.is_windows) System.getenv("TEMP") else null - if (temp != null && temp.contains('\\')) temp else "" - } - val user_home = System.getProperty("user.home", "") - val isabelle_app = System.getProperty("isabelle.app", "") - - default( - default( - default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), - "TEMP_WINDOWS" -> temp_windows), - "HOME" -> user_home), - "ISABELLE_APP" -> "true") - } + synchronized { + if (_settings.isEmpty || _services.isEmpty) { + val isabelle_root1 = + bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") - val settings = - { - val dump = JFile.createTempFile("settings", null) - dump.deleteOnExit - try { - val cmd1 = - if (Platform.is_windows) - List(cygwin_root1 + "\\bin\\bash", "-l", - File.standard_path(isabelle_root1 + "\\bin\\isabelle")) - else - List(isabelle_root1 + "/bin/isabelle") - val cmd = cmd1 ::: List("getenv", "-d", dump.toString) - - val (output, rc) = process_output(process(cmd, env = env, redirect = true)) - if (rc != 0) error(output) + val cygwin_root1 = + if (Platform.is_windows) + bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") + else "" - val entries = - (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { - val i = entry.indexOf('=') - if (i <= 0) entry -> "" - else entry.substring(0, i) -> entry.substring(i + 1) - }).toMap - entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" - } - finally { dump.delete } - } - _settings = Some(settings) - set_cygwin_root() + if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) - val variable = "ISABELLE_SCALA_SERVICES" - val services = - for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) - yield { - def err(msg: String): Nothing = - error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) + def set_cygwin_root() + { + if (Platform.is_windows) + _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) + } + + set_cygwin_root() + + def default(env: Map[String, String], entry: (String, String)): Map[String, String] = + if (env.isDefinedAt(entry._1) || entry._2 == "") env + else env + entry + + val env = + { + val temp_windows = + { + val temp = if (Platform.is_windows) System.getenv("TEMP") else null + if (temp != null && temp.contains('\\')) temp else "" + } + val user_home = System.getProperty("user.home", "") + val isabelle_app = System.getProperty("isabelle.app", "") + + default( + default( + default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), + "TEMP_WINDOWS" -> temp_windows), + "HOME" -> user_home), + "ISABELLE_APP" -> "true") + } + + val settings = + { + val dump = JFile.createTempFile("settings", null) + dump.deleteOnExit try { - Class.forName(name).asInstanceOf[Class[Service]] - .getDeclaredConstructor().newInstance() + val cmd1 = + if (Platform.is_windows) + List(cygwin_root1 + "\\bin\\bash", "-l", + File.standard_path(isabelle_root1 + "\\bin\\isabelle")) + else + List(isabelle_root1 + "/bin/isabelle") + val cmd = cmd1 ::: List("getenv", "-d", dump.toString) + + val (output, rc) = process_output(process(cmd, env = env, redirect = true)) + if (rc != 0) error(output) + + val entries = + (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { + val i = entry.indexOf('=') + if (i <= 0) entry -> "" + else entry.substring(0, i) -> entry.substring(i + 1) + }).toMap + entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } - catch { - case _: ClassNotFoundException => err("Class not found") - case exn: Throwable => err(Exn.message(exn)) + finally { dump.delete } + } + _settings = Some(settings) + set_cygwin_root() + + val variable = "ISABELLE_SCALA_SERVICES" + val services = + for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) + yield { + def err(msg: String): Nothing = + error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) + try { + Class.forName(name).asInstanceOf[Class[Service]] + .getDeclaredConstructor().newInstance() + } + catch { + case _: ClassNotFoundException => err("Class not found") + case exn: Throwable => err(Exn.message(exn)) + } } - } - _services = Some(services) + _services = Some(services) + } } + Scala.Compiler.default_context } /* getenv */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def mkdirs(path: Path): Unit = if (!path.is_dir) { bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } def copy_dir(dir1: Path, dir2: Path): Unit = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: Path): Unit = rm_tree(root.file) def rm_tree(root: JFile) { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit) { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) File.move(dir, old_dir) File.move(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close proc.getErrorStream.close proc.destroy Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout, progress_stderr, progress_limit, strict) } def jconsole(): Process_Result = bash("isabelle_jdk jconsole " + java.lang.ProcessHandle.current().pid).check private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") } } } diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,70 +1,107 @@ (* Title: Pure/System/scala.ML Author: Makarius Support for Scala at runtime. *) signature SCALA = sig - val method: string -> string -> string - val promise_method: string -> string -> string future + val functions: unit -> string list + val check_function: Proof.context -> string * Position.T -> string + val promise_function: string -> string -> string future + val function: string -> string -> string exception Null end; structure Scala: SCALA = struct -(** invoke JVM method via Isabelle/Scala **) +(** invoke Scala functions from ML **) val _ = Session.protocol_handler "isabelle.Scala"; (* pending promises *) val new_id = string_of_int o Counter.make (); val promises = Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); -(* method invocation *) +(* invoke function *) -fun promise_method name arg = +fun promise_function name arg = let + val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; in promise end; -fun method name arg = Future.join (promise_method name arg); +fun function name arg = Future.join (promise_function name arg); (* fulfill *) exception Null; fun fulfill id tag res = let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail "Bad tag"); val promise = Synchronized.change_result promises (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); val _ = Future.fulfill_result promise result; in () end; val _ = Isabelle_Process.protocol_command "Scala.fulfill" (fn [id, tag, res] => fulfill id tag res handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); + +(* registered functions *) + +fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); + +fun check_function ctxt (name, pos) = + let + val kind = Markup.scala_functionN; + val funs = functions (); + in + if member (op =) funs name then + (Context_Position.report ctxt pos (Markup.scala_function name); name) + else + let + val completion_report = + Completion.make_report (name, pos) + (fn completed => + filter completed funs + |> sort_strings + |> map (fn a => (a, (kind, a)))); + in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end + end; + +val _ = Theory.setup + (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ + (Scan.lift Parse.embedded_position) check_function #> + ML_Antiquotation.inline_embedded \<^binding>\scala_function\ + (Args.context -- Scan.lift Parse.embedded_position + >> (uncurry check_function #> ML_Syntax.print_string)) #> + ML_Antiquotation.value_embedded \<^binding>\scala\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => + let val name = check_function ctxt arg + in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); + end; diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,157 +1,203 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle -import java.lang.reflect.{Method, Modifier, InvocationTargetException} -import java.io.{File => JFile} +import java.io.{File => JFile, StringWriter, PrintWriter} -import scala.util.matching.Regex -import scala.tools.nsc.GenericRunnerSettings +import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} +import scala.tools.nsc.interpreter.IMain object Scala { - /* compiler classpath and settings */ + /** compiler **/ - def compiler_classpath(jar_dirs: List[JFile]): String = + object Compiler { - def find_jars(dir: JFile): List[String] = - File.find_files(dir, file => file.getName.endsWith(".jar")). - map(File.absolute_name) + lazy val default_context: Context = context() - val class_path = - space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) + def context( + error: String => Unit = Exn.error, + jar_dirs: List[JFile] = Nil): Context = + { + def find_jars(dir: JFile): List[String] = + File.find_files(dir, file => file.getName.endsWith(".jar")). + map(File.absolute_name) - (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) + val class_path = + for { + prop <- List("isabelle.scala.classpath", "java.class.path") + path = System.getProperty(prop, "") if path != "\"\"" + elem <- space_explode(JFile.pathSeparatorChar, path) + } yield elem + + val settings = new GenericRunnerSettings(error) + settings.classpath.value = + (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) + + new Context(settings) + } + + def default_print_writer: PrintWriter = + new NewLinePrintWriter(new ConsoleWriter, true) + + class Context private [Compiler](val settings: GenericRunnerSettings) + { + override def toString: String = settings.toString + + def interpreter( + print_writer: PrintWriter = default_print_writer, + class_loader: ClassLoader = null): IMain = + { + new IMain(settings, print_writer) + { + override def parentClassLoader: ClassLoader = + if (class_loader == null) super.parentClassLoader + else class_loader + } + } + + def toplevel(source: String): List[String] = + { + val out = new StringWriter + val interp = interpreter(new PrintWriter(out)) + val rep = new interp.ReadEvalPrint + val ok = interp.withLabel("\u0001") { rep.compile(source) } + out.close + + val Error = """(?s)^\S* error: (.*)$""".r + val errors = + space_explode('\u0001', Library.strip_ansi_color(out.toString)). + collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) + + if (!ok && errors.isEmpty) List("Error") else errors + } + + def check(body: String): List[String] = + { + try { toplevel("package test\nobject Test { " + body + " }") } + catch { case ERROR(msg) => List(msg) } + } + } } - def compiler_settings( - error: String => Unit = Exn.error, - jar_dirs: List[JFile] = Nil): GenericRunnerSettings = + def check_yxml(body: String): String = { - val settings = new GenericRunnerSettings(error) - settings.classpath.value = compiler_classpath(jar_dirs) - settings + val errors = Compiler.default_context.check(body) + locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } - /** invoke JVM method via Isabelle/Scala **/ - - /* method reflection */ - - private val Ext = new Regex("(.*)\\.([^.]*)") - private val STRING = Class.forName("java.lang.String") + /** invoke Scala functions from ML **/ - private def get_method(name: String): String => String = - name match { - case Ext(class_name, method_name) => - val m = - try { Class.forName(class_name).getMethod(method_name, STRING) } - catch { - case _: ClassNotFoundException | _: NoSuchMethodException => - error("No such method: " + quote(name)) - } - if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString) - if (m.getReturnType != STRING) error("Bad method return type: " + m.toString) + /* registered functions */ - (arg: String) => { - try { m.invoke(null, arg).asInstanceOf[String] } - catch { - case e: InvocationTargetException if e.getCause != null => - throw e.getCause - } - } - case _ => error("Malformed method name: " + quote(name)) - } + sealed case class Fun(name: String, apply: String => String) + { + override def toString: String = name + } + + lazy val functions: List[Fun] = + Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten - /* method invocation */ + /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } - def method(name: String, arg: String): (Tag.Value, String) = - Exn.capture { get_method(name) } match { - case Exn.Res(f) => - Exn.capture { f(arg) } match { + def function(name: String, arg: String): (Tag.Value, String) = + functions.find(fun => fun.name == name) match { + case Some(fun) => + Exn.capture { fun.apply(arg) } match { case Exn.Res(null) => (Tag.NULL, "") case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) } - case Exn.Exn(e) => (Tag.FAIL, Exn.message(e)) + case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name)) } } /* protocol handler */ class Scala extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(init_session: Session): Unit = synchronized { session = init_session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command("Scala.fulfill", id, tag.id.toString, res) futures -= id } } private def cancel(id: String, future: Future[Unit]) { future.cancel fulfill(id, Scala.Tag.INTERRUPT, "") } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => futures += (id -> Future.fork { - val (tag, result) = Scala.method(name, msg.text) + val (tag, result) = Scala.function(name, msg.text) fulfill(id, tag, result) }) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } val functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } + + +/* registered functions */ + +class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service + +class Functions extends Isabelle_Scala_Functions( + Scala.Fun("echo", identity), + Scala.Fun("scala_check", Scala.check_yxml), + Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml)) diff --git a/src/Pure/System/scala_check.ML b/src/Pure/System/scala_check.ML new file mode 100644 --- /dev/null +++ b/src/Pure/System/scala_check.ML @@ -0,0 +1,22 @@ +(* Title: Pure/System/scala_check.ML + Author: Makarius + +Semantic check of Scala sources. +*) + +signature SCALA_CHECK = +sig + val decl: string -> unit +end; + +structure Scala_Check: SCALA_CHECK = +struct + +fun decl source = + let val errors = + \<^scala>\scala_check\ source + |> YXML.parse_body + |> let open XML.Decode in list string end + in if null errors then () else error (cat_lines errors) end; + +end; diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML +++ b/src/Pure/Thy/bibtex.ML @@ -1,64 +1,64 @@ (* Title: Pure/Thy/bibtex.ML Author: Makarius BibTeX support. *) signature BIBTEX = sig val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit val cite_macro: string Config.T end; structure Bibtex: BIBTEX = struct (* check database *) type message = string * Position.T; fun check_database pos0 database = - Scala.method "isabelle.Bibtex.check_database_yxml" database + \<^scala>\check_bibtex_database\ database |> YXML.parse_body |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0)); fun check_database_output pos0 database = let val (errors, warnings) = check_database pos0 database in errors |> List.app (fn (msg, pos) => Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); warnings |> List.app (fn (msg, pos) => warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) end; (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K "cite"); val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro) #> Thy_Output.antiquotation_raw \<^binding>\cite\ (Scan.lift (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) (fn ctxt => fn (opt, citations) => let val thy = Proof_Context.theory_of ctxt; val bibtex_entries = Present.get_bibtex_entries thy; val _ = if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () else citations |> List.app (fn (name, pos) => if member (op =) bibtex_entries name then () else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); val _ = Context_Position.reports ctxt (map (fn (name, pos) => (pos, Markup.citation name)) citations); val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]"); val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end)); end; diff --git a/src/Pure/Tools/build.ML b/src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML +++ b/src/Pure/Tools/build.ML @@ -1,270 +1,271 @@ (* Title: Pure/Tools/build.ML Author: Makarius Build Isabelle sessions. *) signature BUILD = sig val build: string -> unit end; structure Build: BUILD = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session timing *) fun session_timing session_name verbose f x = let val start = Timing.start (); val y = f x; val timing = Timing.result start; val threads = string_of_int (Multithreading.max_threads ()); val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |> Real.fmt (StringCvt.FIX (SOME 2)); val timing_props = [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; val _ = Protocol_Message.marker "Timing" timing_props; val _ = if verbose then Output.physical_stderr ("Timing " ^ session_name ^ " (" ^ threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") else (); in y end; (* protocol messages *) fun protocol_message props output = (case props of function :: args => if function = Markup.ML_statistics orelse function = Markup.task_statistics then Protocol_Message.marker (#2 function) args else if function = Markup.command_timing then let val name = the_default "" (Properties.get args Markup.nameN); val pos = Position.of_properties args; val {elapsed, ...} = Markup.parse_timing_properties args; val is_significant = Timing.is_relevant_time elapsed andalso elapsed >= Options.default_seconds "command_timing_threshold"; in if is_significant then (case approximative_id name pos of SOME id => Protocol_Message.marker (#2 function) (Markup.command_timing_properties id elapsed) | NONE => ()) else () end else if function = Markup.theory_timing then Protocol_Message.marker (#2 function) args else (case Markup.dest_loading_theory props of SOME name => Protocol_Message.marker_text "loading_theory" name | NONE => Export.protocol_message props output) | [] => raise Output.Protocol_Message props); (* build theories *) fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = let val context = {options = options, symbols = symbols, bibtex_entries = bibtex_entries, last_timing = last_timing}; val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; in if null conds then (Options.set_default options; Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories context qualifier master_dir |> (case Options.string options "profiling" of "" => I | "time" => profile_time | "allocations" => profile_allocations | bad => error ("Bad profiling option: " ^ quote bad)) |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n") end; (* build session *) datatype args = Args of - {symbol_codes: (string * int) list, + {pide: bool, + symbol_codes: (string * int) list, command_timings: Properties.T list, verbose: bool, browser_info: Path.T, document_files: (Path.T * Path.T) list, graph_file: Path.T, parent_name: string, chapter: string, session_name: string, master_dir: Path.T, theories: (Options.T * (string * Position.T) list) list, session_positions: (string * Properties.T) list, session_directories: (string * string) list, doc_names: string list, global_theories: (string * string) list, loaded_theories: string list, bibtex_entries: string list}; -fun decode_args yxml = +fun decode_args pide yxml = let open XML.Decode; val position = Position.of_properties o properties; val (symbol_codes, (command_timings, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir, (theories, (session_positions, (session_directories, (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) = pair (list (pair string int)) (pair (list properties) (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string (pair string (pair (((list (pair Options.decode (list (pair string position)))))) (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list string) (pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) (YXML.parse_body yxml); in - Args {symbol_codes = symbol_codes, command_timings = command_timings, + Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings, verbose = verbose, browser_info = Path.explode browser_info, document_files = map (apply2 Path.explode) document_files, graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, session_name = session_name, master_dir = Path.explode master_dir, theories = theories, session_positions = session_positions, session_directories = session_directories, doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, bibtex_entries = bibtex_entries} end; -fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files, +fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files, graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions, session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = let val symbols = HTML.make_symbols symbol_codes; val _ = - Resources.init_session_base - {session_positions = session_positions, + Resources.init_session + {pide = pide, + session_positions = session_positions, session_directories = session_directories, docs = doc_names, global_theories = global_theories, loaded_theories = loaded_theories}; val _ = Session.init symbols (Options.default_bool "browser_info") browser_info (Options.default_string "document") (Options.default_string "document_output") (Present.document_variants (Options.default ())) document_files graph_file parent_name (chapter, session_name) verbose; val last_timing = get_timings (fold update_timings command_timings empty_timings); val res1 = theories |> (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir) |> session_timing session_name verbose |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); val _ = Par_Exn.release_all [res1, res2]; val _ = if session_name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; (* command-line tool *) fun inline_errors exn = Runtime.exn_message_list exn |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg)); fun build args_file = let val _ = SHA1.test_samples (); val _ = Options.load_default (); val _ = Isabelle_Process.init_options (); - val args = decode_args (File.read (Path.explode args_file)); + val args = decode_args false (File.read (Path.explode args_file)); val _ = Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message build_session args handle exn => (inline_errors exn; Exn.reraise exn); val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; val _ = Options.reset_default (); in () end; (* PIDE version *) -fun build_session_finished errs = - XML.Encode.list XML.Encode.string errs - |> Output.protocol_message Markup.build_session_finished; - val _ = Isabelle_Process.protocol_command "build_session" (fn [args_yxml] => let - val args = decode_args args_yxml; - val errs = - Future.interruptible_task (fn () => (build_session args; [])) () handle exn => - (Runtime.exn_message_list exn handle _ (*sic!*) => - (build_session_finished ["CRASHED"]; - raise Isabelle_Process.EXIT 2)); - val _ = build_session_finished errs; + val args = decode_args true args_yxml; + fun exec e = + if can Theory.get_pure () then + Isabelle_Thread.fork + {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), + interrupts = false} e + |> ignore + else e (); in - if null errs - then raise Isabelle_Process.STOP - else raise Isabelle_Process.EXIT 1 + exec (fn () => + (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn => + ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) + |> let open XML.Encode in pair int (list string) end + |> Output.protocol_message Markup.build_session_finished) end | _ => raise Match); end; diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala +++ b/src/Pure/Tools/build.scala @@ -1,957 +1,965 @@ /* Title: Pure/Tools/build.scala Author: Makarius Options: :folding=explicit: Build and manage Isabelle sessions. */ package isabelle import scala.collection.{SortedSet, mutable} import scala.annotation.tailrec object Build { /** auxiliary **/ /* persistent build info */ sealed case class Session_Info( sources: String, input_heaps: List[String], output_heap: Option[String], return_code: Int) { def ok: Boolean = return_code == 0 } /* queue with scheduling information */ private object Queue { type Timings = (List[Properties.T], Double) def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings = { val no_timings: Timings = (Nil, 0.0) store.access_database(session_name) match { case None => no_timings case Some(db) => def ignore_error(msg: String) = { progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg)) no_timings } try { val command_timings = store.read_command_timings(db, session_name) val session_timing = store.read_session_timing(db, session_name) match { case Markup.Elapsed(t) => t case _ => 0.0 } (command_timings, session_timing) } catch { case ERROR(msg) => ignore_error(msg) case exn: java.lang.Error => ignore_error(Exn.message(exn)) case _: XML.Error => ignore_error("") } finally { db.close } } } def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double]) : Map[String, Double] = { val maximals = sessions_structure.build_graph.maximals.toSet def desc_timing(session_name: String): Double = { if (maximals.contains(session_name)) timing(session_name) else { val descendants = sessions_structure.build_descendants(List(session_name)).toSet val g = sessions_structure.build_graph.restrict(descendants) (0.0 :: g.maximals.flatMap(desc => { val ps = g.all_preds(List(desc)) if (ps.exists(p => timing.get(p).isEmpty)) None else Some(ps.map(timing(_)).sum) })).max } } timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0) } def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store) : Queue = { val graph = sessions_structure.build_graph val names = graph.keys val timings = names.map(name => (name, load_timings(progress, store, name))) val command_timings = timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil) val session_timing = make_session_timing(sessions_structure, timings.map({ case (name, (_, t)) => (name, t) }).toMap) object Ordering extends scala.math.Ordering[String] { def compare_timing(name1: String, name2: String): Int = { val t1 = session_timing(name1) val t2 = session_timing(name2) if (t1 == 0.0 || t2 == 0.0) 0 else t1 compare t2 } def compare(name1: String, name2: String): Int = compare_timing(name2, name1) match { case 0 => sessions_structure(name2).timeout compare sessions_structure(name1).timeout match { case 0 => name1 compare name2 case ord => ord } case ord => ord } } new Queue(graph, SortedSet(names: _*)(Ordering), command_timings) } } private class Queue( graph: Graph[String, Sessions.Info], order: SortedSet[String], val command_timings: String => List[Properties.T]) { def is_inner(name: String): Boolean = !graph.is_maximal(name) def is_empty: Boolean = graph.is_empty def - (name: String): Queue = new Queue(graph.del_node(name), order - name, // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? command_timings) def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] = { val it = order.iterator.dropWhile(name => skip(name) || !graph.defined(name) // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!? || !graph.is_minimal(name)) if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) } else None } } /* PIDE protocol handler */ /* job: running prover process */ private class Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, verbose: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { val options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf") graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display) private val export_tmp_dir = Isabelle_System.tmp_dir("export") private val export_consumer = Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), pair(list(string), list(string)))))))))))))))))( (Symbol.codes, (command_timings, (verbose, (store.browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (base.doc_names, (base.global_theories.toList, (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))) }) val env = Isabelle_System.settings() + ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) + ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil - if (options.bool("pide_build")) { + if (options.bool("pide_session")) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val build_session_errors: Promise[List[String]] = Future.promise val stdout = new StringBuilder(1000) val messages = new mutable.ListBuffer[String] val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] session.init_protocol_handler(new Session.Protocol_Handler { override def exit() { build_session_errors.cancel } private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { - val errors = + val (rc, errors) = try { - for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text))) - yield { - val prt = Protocol_Message.expose_no_reports(err) - Pretty.string_of(prt, metric = Symbol.Metric) + val (rc, errs) = + { + import XML.Decode._ + pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } + val errors = + for (err <- errs) yield { + val prt = Protocol_Message.expose_no_reports(err) + Pretty.string_of(prt, metric = Symbol.Metric) + } + (rc, errors) } - catch { case ERROR(err) => List(err) } + catch { case ERROR(err) => (2, List(err)) } + + session.protocol_command("Prover.stop", rc.toString) build_session_errors.fulfill(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(name) => progress.theory(Progress.Theory(name, session = session_name)) true case _ => false } private def export(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.bytes) true case _ => false } private def command_timing(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Command_Timing(props) => command_timings += props; true case _ => false } private def theory_timing(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Theory_Timing(props) => theory_timings += props; true case _ => false } private def ml_stats(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.ML_Statistics(props) => runtime_statistics += props; true case _ => false } private def task_stats(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Task_Statistics(props) => task_statistics += props; true case _ => false } val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export, Markup.Command_Timing.name -> command_timing, Markup.Theory_Timing.name -> theory_timing, Markup.ML_Statistics.name -> ml_stats, Markup.Task_Statistics.name -> task_stats) }) session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (Protocol.is_exported(message)) { messages += Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric)) } case _ => } val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val errors = Isabelle_Thread.interrupt_handler(_ => process.terminate) { Exn.capture { process.await_startup } match { case Exn.Res(_) => session.protocol_command("build_session", args_yxml) build_session_errors.join_result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } val process_output = stdout.toString :: messages.toList ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output) errors match { case Exn.Res(Nil) => result case Exn.Res(errs) => result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result case Exn.Exn(exn) => throw exn } } else { val args_file = Isabelle_System.tmp_file("build") File.write(args_file, args_yxml) val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) val eval_main = Command_Line.ML_tool(eval_build :: eval_store) val process = ML_Process(options, deps.sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env, cleanup = () => args_file.delete) Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.result( progress_stdout = { case Protocol.Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, session = session_name)) case Protocol.Export.Marker((args, path)) => val body = try { Bytes.read(path) } catch { case ERROR(msg) => error("Failed to read export " + quote(args.compound_name) + "\n" + msg) } path.file.delete export_consumer(session_name, args, body) case _ => }, progress_limit = options.int("process_output_limit") match { case 0 => None case m => Some(m * 1000000L) }, strict = false) } } } def terminate: Unit = future_result.cancel def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout > Time.zero) Some(Event_Timer.request(Time.now() + info.timeout) { terminate }) else None } def join: (Process_Result, Option[String]) = { val result0 = future_result.join val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text) match { case Nil => result0 case errs => result0.errors(errs).error_rc } Isabelle_System.rm_tree(export_tmp_dir) if (result1.ok) Present.finish(progress, store.browser_info, graph_file, info, session_name) graph_file.delete val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel } val result2 = if (result1.interrupted) { if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout else result1.error(Output.error_message_text("Interrupt")) } else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } /** build with results **/ class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)]) { def sessions: Set[String] = results.keySet def cancelled(name: String): Boolean = results(name)._1.isEmpty def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1)) def info(name: String): Sessions.Info = results(name)._2 val rc: Int = (0 /: results.iterator.map( { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _) def ok: Boolean = rc == 0 override def toString: String = rc.toString } def build( options: Options, progress: Progress = new Progress, check_unknown_files: Boolean = false, build_heap: Boolean = false, clean_build: Boolean = false, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Sessions.Info] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, fresh_build: Boolean = false, no_build: Boolean = false, soft_build: Boolean = false, verbose: Boolean = false, export_files: Boolean = false, requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty): Results = { val build_options = options + "ML_statistics" + "completion_limit=0" + "editor_tracing_messages=0" + "pide_reports=false" val store = Sessions.store(build_options) Isabelle_Fonts.init() /* session selection and dependencies */ val full_sessions = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) def sources_stamp(deps: Sessions.Deps, session_name: String): String = { val digests = full_sessions(session_name).meta_digest :: deps.sources(session_name) ::: deps.imported_sources(session_name) SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } val selection1 = Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions) ++ selection val deps = { val deps0 = Sessions.deps(full_sessions.selection(selection1), progress = progress, inlined_files = true, verbose = verbose, list_files = list_files, check_keywords = check_keywords).check_errors if (soft_build && !fresh_build) { val outdated = deps0.sessions_structure.build_topological_order.flatMap(name => store.access_database(name) match { case Some(db) => using(db)(store.read_build(_, name)) match { case Some(build) if build.ok && build.sources == sources_stamp(deps0, name) => None case _ => Some(name) } case None => Some(name) }) Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)), progress = progress, inlined_files = true).check_errors } else deps0 } /* check unknown files */ if (check_unknown_files) { val source_files = (for { (_, base) <- deps.session_bases.iterator (path, _) <- base.sources.iterator } yield path).toList val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file) val unknown_files = Mercurial.check_files(source_files)._2. filterNot(path => exclude_files.contains(path.canonical_file)) if (unknown_files.nonEmpty) { progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" + unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", "")) } } /* main build process */ val queue = Queue(progress, deps.sessions_structure, store) store.prepare_output_dir() if (clean_build) { for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection1))) { val (relevant, ok) = store.clean_output(name) if (relevant) { if (ok) progress.echo("Cleaned " + name) else progress.echo(name + " FAILED to clean") } } } // scheduler loop case class Result( current: Boolean, heap_digest: Option[String], process: Option[Process_Result], info: Sessions.Info) { def ok: Boolean = process match { case None => false case Some(res) => res.rc == 0 } } def sleep() { Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep } } val numa_nodes = new NUMA.Nodes(numa_shuffling) @tailrec def loop( pending: Queue, running: Map[String, (List[String], Job)], results: Map[String, Result]): Map[String, Result] = { def used_node(i: Int): Boolean = running.iterator.exists( { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i }) if (pending.is_empty) results else { if (progress.stopped) { for ((_, (_, job)) <- running) job.terminate } running.find({ case (_, (_, job)) => job.is_finished }) match { case Some((session_name, (input_heaps, job))) => //{{{ finish job val (process_result, heap_digest) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail") process_result.copy( out_lines = "(see also " + store.output_log(session_name).file.toString + ")" :: (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0))) } // write log file if (process_result.ok) { File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) } else File.write(store.output_log(session_name), terminate_lines(log_lines)) // write database { val build_log = Build_Log.Log_File(session_name, process_result.out_lines). parse_session_info( command_timings = true, theory_timings = true, ml_statistics = true, task_statistics = true) using(store.open_database(session_name, output = true))(db => store.write_session_info(db, session_name, build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest, process_result.rc))) } // messages process_result.err_lines.foreach(progress.echo) if (process_result.ok) progress.echo( "Finished " + session_name + " (" + process_result.timing.message_resources + ")") else { progress.echo(session_name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out) } loop(pending - session_name, running - session_name, results + (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt) match { case Some((session_name, info)) => val ancestor_results = deps.sessions_structure.build_requirements(List(session_name)). filterNot(_ == session_name).map(results(_)) val ancestor_heaps = ancestor_results.flatMap(_.heap_digest) val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) val (current, heap_digest) = { store.access_database(session_name) match { case Some(db) => using(db)(store.read_build(_, session_name)) match { case Some(build) => val heap_digest = store.find_heap_digest(session_name) val current = !fresh_build && build.ok && build.sources == sources_stamp(deps, session_name) && build.input_heaps == ancestor_heaps && build.output_heap == heap_digest && !(do_store && heap_digest.isEmpty) (current, heap_digest) case None => (false, None) } case None => (false, None) } } val all_current = current && ancestor_results.forall(_.current) if (all_current) loop(pending - session_name, running, results + (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info))) else if (no_build) { if (verbose) progress.echo("Skipping " + session_name + " ...") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") store.clean_output(session_name) using(store.open_database(session_name, output = true))( store.init_session_info(_, session_name)) val numa_node = numa_nodes.next(used_node) val job = new Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) } else { progress.echo(session_name + " CANCELLED") loop(pending - session_name, running, results + (session_name -> Result(false, heap_digest, None, info))) } case None => sleep(); loop(pending, running, results) } ///}}} case None => sleep(); loop(pending, running, results) } } } /* build results */ val results0 = if (deps.is_empty) { progress.echo_warning("Nothing to build") Map.empty[String, Result] } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } val results = new Results( (for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap) if (export_files) { for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) { val info = results.info(name) if (info.export_files.nonEmpty) { progress.echo("Exporting " + info.name + " ...") for ((dir, prune, pats) <- info.export_files) { Export.export_files(store, name, info.dir + dir, progress = if (verbose) progress else new Progress, export_prune = prune, export_patterns = pats) } } } } if (results.rc != 0 && (verbose || !no_build)) { val unfinished = (for { name <- results.sessions.iterator if !results(name).ok } yield name).toList.sorted progress.echo("Unfinished session(s): " + commas(unfinished)) } /* global browser info */ if (!no_build) { val browser_chapters = (for { (name, result) <- results0.iterator if result.ok info = full_sessions(name) if info.options.bool("browser_info") } yield (info.chapter, (name, info.description))).toList.groupBy(_._1). map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty) for ((chapter, entries) <- browser_chapters) Present.update_chapter_index(store.browser_info, chapter, entries) if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info) } results } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil var all_sessions = false var build_heap = false var clean_build = false var dirs: List[Path] = Nil var export_files = false var fresh_build = false var session_groups: List[String] = Nil var max_jobs = 1 var check_keywords: Set[String] = Set.empty var list_files = false var no_build = false var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b build heap images -c clean build -d DIR include session directory -e export files from session specification into file-system -f fresh build -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files -n no build -- test dependencies only -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Build and manage Isabelle sessions, depending on implicit settings: """ + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n", "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "b" -> (_ => build_heap = true), "c" -> (_ => clean_build = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e" -> (_ => export_files = true), "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "j:" -> (arg => max_jobs = Value.Int.parse(arg)), "k:" -> (arg => check_keywords = check_keywords + arg), "l" -> (_ => list_files = true), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo( "Started at " + Build_Log.print_date(start_date) + " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")") progress.echo(Build_Log.Settings.show() + "\n") } val results = progress.interrupt_handler { build(options, progress = progress, check_unknown_files = Mercurial.is_repository(Path.explode("~~")), build_heap = build_heap, clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, fresh_build = fresh_build, no_build = no_build, soft_build = soft_build, verbose = verbose, export_files = export_files, requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) /* build logic image */ def build_logic(options: Options, logic: String, progress: Progress = new Progress, build_heap: Boolean = false, dirs: List[Path] = Nil, fresh: Boolean = false, strict: Boolean = false): Int = { val rc = if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs, sessions = List(logic)).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh, dirs = dirs, sessions = List(logic)).rc } if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc } } diff --git a/src/Pure/library.scala b/src/Pure/library.scala --- a/src/Pure/library.scala +++ b/src/Pure/library.scala @@ -1,276 +1,279 @@ /* Title: Pure/library.scala Author: Makarius Basic library. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.util.matching.Regex object Library { /* resource management */ def using[A <: AutoCloseable, B](a: A)(f: A => B): B = { try { f(a) } finally { if (a != null) a.close() } } /* integers */ private val small_int = 10000 private lazy val small_int_table = { val array = new Array[String](small_int) for (i <- 0 until small_int) array(i) = i.toString array } def is_small_int(s: String): Boolean = { val len = s.length 1 <= len && len <= 4 && s.forall(c => '0' <= c && c <= '9') && (len == 1 || s(0) != '0') } def signed_string_of_long(i: Long): String = if (0 <= i && i < small_int) small_int_table(i.toInt) else i.toString def signed_string_of_int(i: Int): String = if (0 <= i && i < small_int) small_int_table(i) else i.toString /* separated chunks */ def separate[A](s: A, list: List[A]): List[A] = { val result = new mutable.ListBuffer[A] var first = true for (x <- list) { if (first) { first = false result += x } else { result += s result += x } } result.toList } def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] = new Iterator[CharSequence] { private val end = source.length private def next_chunk(i: Int): Option[(CharSequence, Int)] = { if (i < end) { var j = i; do j += 1 while (j < end && !sep(source.charAt(j))) Some((source.subSequence(i + 1, j), j)) } else None } private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) def hasNext(): Boolean = state.isDefined def next(): CharSequence = state match { case Some((s, i)) => state = next_chunk(i); s case None => Iterator.empty.next() } } def space_explode(sep: Char, str: String): List[String] = separated_chunks(_ == sep, str).map(_.toString).toList /* lines */ def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n") def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") def split_lines(str: String): List[String] = space_explode('\n', str) def prefix_lines(prfx: String, str: String): String = if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source) if (lines.hasNext) lines.next.toString else "" } def encode_lines(s: String): String = s.replace('\n', '\u000b') def decode_lines(s: String): String = s.replace('\u000b', '\n') /* strings */ def make_string(f: StringBuilder => Unit): String = { val s = new StringBuilder f(s) s.toString } def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None def try_unsuffix(sffx: String, s: String): Option[String] = if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s def trim_line(s: String): String = if (s.endsWith("\r\n")) s.substring(0, s.length - 2) else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s def trim_split_lines(s: String): List[String] = split_lines(trim_line(s)).map(trim_line) def isolate_substring(s: String): String = new String(s.toCharArray) + def strip_ansi_color(s: String): String = + s.replaceAll("""\u001b\[\d+m""", "") + /* quote */ def single_quote(s: String): String = "'" + s + "'" def quote(s: String): String = "\"" + s + "\"" def try_unquote(s: String): Option[String] = if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) else None def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") /* CharSequence */ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence { require(0 <= start && start <= end && end <= text.length) def this(text: CharSequence) = this(text, 0, text.length) def length: Int = end - start def charAt(i: Int): Char = text.charAt(end - i - 1) def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (i <- 0 until length) buf.append(charAt(i)) buf.toString } } class Line_Termination(text: CharSequence) extends CharSequence { def length: Int = text.length + 1 def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) def subSequence(i: Int, j: Int): CharSequence = if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1)) else text.subSequence(i, j) override def toString: String = text.toString + "\n" } /* regular expressions */ def make_regex(s: String): Option[Regex] = try { Some(new Regex(s)) } catch { case ERROR(_) => None } def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c) def escape_regex(s: String): String = if (s.exists(is_regex_meta)) { (for (c <- s.iterator) yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString } else s /* lists */ def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = (xs.takeWhile(pred), xs.dropWhile(pred)) def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = { val rev_xs = xs.reverse (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse) } def trim[A](pred: A => Boolean, xs: List[A]): List[A] = take_suffix(pred, take_prefix(pred, xs)._2)._1 def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) def merge[A](xs: List[A], ys: List[A]): List[A] = if (xs.eq(ys)) xs else if (xs.isEmpty) ys else ys.foldRight(xs)(Library.insert(_)(_)) def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) result.toList } def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] @tailrec def dups(rest: List[A]): Unit = rest match { case Nil => case x :: xs => if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x dups(xs) } dups(lst) result.toList } def replicate[A](n: Int, a: A): List[A] = if (n < 0) throw new IllegalArgumentException else if (n == 0) Nil else { val res = new mutable.ListBuffer[A] (1 to n).foreach(_ => res += a) res.toList } /* proper values */ def proper_string(s: String): Option[String] = if (s == null || s == "") None else Some(s) def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) } diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala +++ b/src/Tools/jEdit/src/jedit_lib.scala @@ -1,391 +1,397 @@ /* Title: Tools/jEdit/src/jedit_lib.scala Author: Makarius Misc library functions for jEdit. */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension} import java.awt.event.{InputEvent, KeyEvent, KeyListener} import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.util.parsing.input.CharSequenceReader import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} import org.gjt.sp.jedit.gui.KeyEventWorkaround import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} object JEdit_Lib { + /* jEdit directories */ + + def directories: List[JFile] = + (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) + + /* location within multi-screen environment */ final case class Screen_Location(point: Point, bounds: Rectangle) { def relative(parent: Component, size: Dimension): Point = { val w = size.width val h = size.height val x0 = parent.getLocationOnScreen.x val y0 = parent.getLocationOnScreen.y val x1 = x0 + parent.getWidth - w val y1 = y0 + parent.getHeight - h val x2 = point.x min (bounds.x + bounds.width - w) val y2 = point.y min (bounds.y + bounds.height - h) val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) SwingUtilities.convertPointFromScreen(location, parent) location } } def screen_location(component: Component, point: Point): Screen_Location = { val screen_point = new Point(point.x, point.y) SwingUtilities.convertPointToScreen(screen_point, component) val ge = GraphicsEnvironment.getLocalGraphicsEnvironment val screen_bounds = (for { device <- ge.getScreenDevices.iterator config <- device.getConfigurations.iterator bounds = config.getBounds } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds Screen_Location(screen_point, screen_bounds) } /* window geometry measurement */ private lazy val dummy_window = new JWindow final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) { def deco_width: Int = width - inner_width def deco_height: Int = height - inner_height } def window_geometry(outer: Container, inner: Component): Window_Geometry = { GUI_Thread.require {} val old_content = dummy_window.getContentPane dummy_window.setContentPane(outer) dummy_window.pack dummy_window.revalidate val geometry = Window_Geometry( dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) dummy_window.setContentPane(old_content) geometry } /* files */ def is_file(name: String): Boolean = VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] def check_file(name: String): Option[JFile] = if (is_file(name)) Some(new JFile(name)) else None /* buffers */ def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } def buffer_reader(buffer: JEditBuffer): CharSequenceReader = Scan.char_reader(buffer.getSegment(0, buffer.getLength)) def buffer_mode(buffer: JEditBuffer): String = { val mode = buffer.getMode if (mode == null) "" else { val name = mode.getName if (name == null) "" else name } } def buffer_line_manager(buffer: JEditBuffer): LineManager = Untyped.get[LineManager](buffer, "lineMgr") def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = { val undo_in_progress = buffer.isUndoInProgress def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) } try { set(true); body } finally { set(undo_in_progress) } } /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator def jedit_buffer(name: String): Option[Buffer] = jedit_buffers().find(buffer => buffer_name(buffer) == name) def jedit_buffer(name: Document.Node.Name): Option[Buffer] = jedit_buffer(name.node) def jedit_views(): Iterator[View] = jEdit.getViews().iterator def jedit_view(view: View = null): View = if (view == null) jEdit.getActiveView() else view def jedit_edit_panes(view: View): Iterator[EditPane] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null) def jedit_text_areas(view: View): Iterator[JEditTextArea] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) def jedit_text_areas(): Iterator[JEditTextArea] = jedit_views().flatMap(jedit_text_areas) def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.beginCompoundEdit(); body } finally { buffer.endCompoundEdit() } } /* get text */ def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } /* point range */ def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = if (offset < 0) Text.Range.offside else buffer_lock(buffer) { def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) try { val c = text(offset) if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) Text.Range(offset, offset + 2) else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) Text.Range(offset - 1, offset + 1) else Text.Range(offset, offset + 1) } catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } } /* text ranges */ def buffer_range(buffer: JEditBuffer): Text.Range = Text.Range(0, buffer.getLength) def line_range(buffer: JEditBuffer, line: Int): Text.Range = Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength) def caret_range(text_area: TextArea): Text.Range = point_range(text_area.getBuffer, text_area.getCaretPosition) def visible_range(text_area: TextArea): Option[Text.Range] = { val buffer = text_area.getBuffer val n = text_area.getVisibleLines if (n > 0) { val start = text_area.getScreenLineStartOffset(0) val raw_end = text_area.getScreenLineEndOffset(n - 1) val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength Some(Text.Range(start, end)) } else None } def invalidate_range(text_area: TextArea, range: Text.Range) { val buffer = text_area.getBuffer buffer_range(buffer).try_restrict(range) match { case Some(range1) if !range1.is_singularity => try { text_area.invalidateLineRange( buffer.getLineOfOffset(range1.start), buffer.getLineOfOffset(range1.stop)) } catch { case _: ArrayIndexOutOfBoundsException => } case _ => } } def invalidate(text_area: TextArea) { val visible_lines = text_area.getVisibleLines if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) } /* graphics range */ case class Gfx_Range(x: Int, y: Int, length: Int) // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { val metric = pretty_metric(text_area.getPainter) val char_width = (metric.unit * metric.average).round.toInt val buffer = text_area.getBuffer val end = buffer.getLength val stop = range.stop val (p, q, r) = try { val p = text_area.offsetToXY(range.start) val (q, r) = if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) else if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) else (text_area.offsetToXY(stop), 0) (p, q, r) } catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } if (p != null && q != null && p.x < q.x + r && p.y == q.y) Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) else None } /* pixel range */ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = { // coordinates wrt. inner painter component val painter = text_area.getPainter if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) { val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) gfx_range(text_area, range) match { case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } } else None } else None } /* pretty text metric */ abstract class Pretty_Metric extends Pretty.Metric { def average: Double } def pretty_metric(painter: TextAreaPainter): Pretty_Metric = new Pretty_Metric { def string_width(s: String): Double = painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth val unit: Double = string_width(Symbol.space) max 1.0 val average: Double = string_width("mix") / (3 * unit) def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit } /* icons */ def load_icon(name: String): Icon = { val name1 = if (name.startsWith("idea-icons/")) { val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString "jar:" + file + "!/" + name } else name val icon = GUIUtilities.loadIcon(name1) if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) else icon } def load_image_icon(name: String): ImageIcon = load_icon(name) match { case icon: ImageIcon => icon case _ => error("Bad image icon: " + name) } /* key event handling */ def request_focus_view(alt_view: View = null) { isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view) } def propagate_key(view: View, evt: KeyEvent) { if (view != null && !evt.isConsumed) view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) } def key_listener( key_typed: KeyEvent => Unit = _ => (), key_pressed: KeyEvent => Unit = _ => (), key_released: KeyEvent => Unit = _ => ()): KeyListener = { def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit) { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) handle(evt) } new KeyListener { def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) } def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) } def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) } } } def special_key(evt: KeyEvent): Boolean = { // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java val mod = evt.getModifiersEx (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 || (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED || (mod & InputEvent.META_DOWN_MASK) != 0 } } diff --git a/src/Tools/jEdit/src/scala_console.scala b/src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala +++ b/src/Tools/jEdit/src/scala_console.scala @@ -1,197 +1,182 @@ /* Title: Tools/jEdit/src/scala_console.scala Author: Makarius Scala instance of Console plugin. */ package isabelle.jedit import isabelle._ import console.{Console, ConsolePane, Shell, Output} - -import org.gjt.sp.jedit.{jEdit, JARClassLoader} -import org.gjt.sp.jedit.MiscUtilities - -import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter} - -import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} -import scala.tools.nsc.interpreter.IMain -import scala.collection.mutable +import org.gjt.sp.jedit.JARClassLoader +import java.io.{OutputStream, Writer, PrintWriter} class Scala_Console extends Shell("Scala") { - /* reconstructed jEdit/plugin classpath */ - - private def jar_dirs: List[JFile] = - (proper_string(jEdit.getSettingsDirectory).toList ::: - proper_string(jEdit.getJEditHome).toList).map(new JFile(_)) - - /* global state -- owned by GUI thread */ @volatile private var interpreters = Map.empty[Console, Interpreter] @volatile private var global_console: Console = null @volatile private var global_out: Output = null @volatile private var global_err: Output = null private val console_stream = new OutputStream { val buf = new StringBuilder(100) override def flush() { val s = buf.synchronized { val s = buf.toString; buf.clear; s } val str = UTF8.decode_permissive(s) GUI_Thread.later { if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output } override def close() { flush () } def write(byte: Int) { val c = byte.toChar buf.synchronized { buf.append(c) } if (c == '\n') flush() } } private val console_writer = new Writer { def flush() { console_stream.flush() } def close() { console_stream.flush() } def write(cbuf: Array[Char], off: Int, len: Int) { if (len > 0) { UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) } } } private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = { global_console = console global_out = out global_err = if (err == null) out else err try { scala.Console.withErr(console_stream) { scala.Console.withOut(console_stream) { e } } } finally { console_stream.flush global_console = null global_out = null global_err = null } } private def report_error(str: String) { if (global_console == null || global_err == null) isabelle.Output.writeln(str) else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } /* interpreter thread */ private abstract class Request private case class Start(console: Console) extends Request private case class Execute(console: Console, out: Output, err: Output, command: String) extends Request private class Interpreter { private val running = Synchronized[Option[Thread]](None) def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) } - private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs) - - private val interp = new IMain(settings, new PrintWriter(console_writer, true)) - { - override def parentClassLoader = new JARClassLoader - } + private val interp = + Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). + interpreter( + print_writer = new PrintWriter(console_writer, true), + class_loader = new JARClassLoader) val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") { case Start(console) => interp.bind("view", "org.gjt.sp.jedit.View", console.getView) interp.bind("console", "console.Console", console) interp.interpret("import isabelle._; import isabelle.jedit._") true case Execute(console, out, err, command) => with_console(console, out, err) { try { running.change(_ => Some(Thread.currentThread())) interp.interpret(command) } finally { running.change(_ => None) Exn.Interrupt.dispose() } GUI_Thread.later { if (err != null) err.commandDone() out.commandDone() } true } } } /* jEdit console methods */ override def openConsole(console: Console) { val interp = new Interpreter interp.thread.send(Start(console)) interpreters += (console -> interp) } override def closeConsole(console: Console) { interpreters.get(console) match { case Some(interp) => interp.interrupt interp.thread.shutdown interpreters -= console case None => } } override def printInfoMessage(out: Output) { out.print(null, "This shell evaluates Isabelle/Scala expressions.\n\n" + "The contents of package isabelle and isabelle.jedit are imported.\n" + "The following special toplevel bindings are provided:\n" + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + " console -- jEdit Console plugin\n" + " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") } override def printPrompt(console: Console, out: Output) { out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") } override def execute(console: Console, input: String, out: Output, err: Output, command: String) { interpreters(console).thread.send(Execute(console, out, err, command)) } override def stop(console: Console) { interpreters.get(console).foreach(_.interrupt) } }

code: 0x01d4ab group: letter \ code: 0x01d4ac group: letter \ code: 0x00211b group: letter \ code: 0x01d4ae group: letter \ code: 0x01d4af group: letter \ code: 0x01d4b0 group: letter \ code: 0x01d4b1 group: letter \ code: 0x01d4b2 group: letter \ code: 0x01d4b3 group: letter \ code: 0x01d4b4 group: letter \ code: 0x01d4b5 group: letter \ code: 0x01d5ba group: letter \ code: 0x01d5bb group: letter \ code: 0x01d5bc group: letter \ code: 0x01d5bd group: letter \ code: 0x01d5be group: letter \ code: 0x01d5bf group: letter \ code: 0x01d5c0 group: letter \ code: 0x01d5c1 group: letter \ code: 0x01d5c2 group: letter \ code: 0x01d5c3 group: letter \ code: 0x01d5c4 group: letter \ code: 0x01d5c5 group: letter \ code: 0x01d5c6 group: letter \ code: 0x01d5c7 group: letter \ code: 0x01d5c8 group: letter \