| author | blanchet | 
| Wed, 08 Apr 2015 18:43:43 +0200 | |
| changeset 59959 | 1e3383a5204b | 
| parent 59891 | 9ce697050455 | 
| child 60749 | f727b99faaf7 | 
| permissions | -rwxr-xr-x | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 1 | #!/usr/bin/env bash | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 2 | # | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 3 | # Author: Makarius | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 4 | # | 
| 42899 | 5 | # build-jars - build Isabelle/Scala | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 6 | # | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 7 | # Requires proper Isabelle settings environment. | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 8 | |
| 43320 | 9 | ## sources | 
| 10 | ||
| 11 | declare -a SOURCES=( | |
| 56695 
963732291084
consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
 wenzelm parents: 
56693diff
changeset | 12 | Concurrent/consumer_thread.scala | 
| 43660 | 13 | Concurrent/counter.scala | 
| 56768 | 14 | Concurrent/event_timer.scala | 
| 43320 | 15 | Concurrent/future.scala | 
| 56693 | 16 | Concurrent/mailbox.scala | 
| 59136 
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
 wenzelm parents: 
58928diff
changeset | 17 | Concurrent/par_list.scala | 
| 43320 | 18 | Concurrent/simple_thread.scala | 
| 56685 | 19 | Concurrent/synchronized.scala | 
| 57647 | 20 | GUI/color_value.scala | 
| 21 | GUI/gui.scala | |
| 22 | GUI/gui_thread.scala | |
| 23 | GUI/html5_panel.scala | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
57905diff
changeset | 24 | GUI/jfx_gui.scala | 
| 57647 | 25 | GUI/popup.scala | 
| 26 | GUI/system_dialog.scala | |
| 27 | GUI/wrap_panel.scala | |
| 55511 
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
 wenzelm parents: 
55497diff
changeset | 28 | General/antiquote.scala | 
| 54439 | 29 | General/bytes.scala | 
| 55673 
0286219c1261
clarified module location (again, see 763d35697338);
 wenzelm parents: 
55511diff
changeset | 30 | General/completion.scala | 
| 43320 | 31 | General/exn.scala | 
| 48411 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 wenzelm parents: 
48410diff
changeset | 32 | General/file.scala | 
| 46611 | 33 | General/graph.scala | 
| 59244 
19b5fc4b2b38
more uniform support for graph display in ML/Scala;
 wenzelm parents: 
59232diff
changeset | 34 | General/graph_display.scala | 
| 51098 | 35 | General/graphics_file.scala | 
| 43320 | 36 | General/linear_set.scala | 
| 56800 | 37 | General/long_name.scala | 
| 52975 | 38 | General/multi_map.scala | 
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: 
56768diff
changeset | 39 | General/output.scala | 
| 43600 
4ac04bf9ff89
abstract algebra of file paths in Scala (cf. path.ML);
 wenzelm parents: 
43523diff
changeset | 40 | General/path.scala | 
| 43320 | 41 | General/position.scala | 
| 42 | General/pretty.scala | |
| 43780 | 43 | General/properties.scala | 
| 43320 | 44 | General/scan.scala | 
| 45 | General/sha1.scala | |
| 46 | General/symbol.scala | |
| 45674 | 47 | General/time.scala | 
| 45666 | 48 | General/timing.scala | 
| 57647 | 49 | General/untyped.scala | 
| 56501 
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
 wenzelm parents: 
56429diff
changeset | 50 | General/url.scala | 
| 56599 | 51 | General/word.scala | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: 
52667diff
changeset | 52 | General/xz_file.scala | 
| 43320 | 53 | Isar/keyword.scala | 
| 54 | Isar/outer_syntax.scala | |
| 55 | Isar/parse.scala | |
| 56 | Isar/token.scala | |
| 55497 | 57 | ML/ml_lex.scala | 
| 59362 | 58 | PIDE/batch_session.scala | 
| 43320 | 59 | PIDE/command.scala | 
| 57905 
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
 wenzelm parents: 
57900diff
changeset | 60 | PIDE/command_span.scala | 
| 43320 | 61 | PIDE/document.scala | 
| 52530 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
 wenzelm parents: 
52444diff
changeset | 62 | PIDE/document_id.scala | 
| 52971 
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
 wenzelm parents: 
52671diff
changeset | 63 | PIDE/editor.scala | 
| 45670 | 64 | PIDE/markup.scala | 
| 43320 | 65 | PIDE/markup_tree.scala | 
| 45709 
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
 wenzelm parents: 
45674diff
changeset | 66 | PIDE/protocol.scala | 
| 59713 | 67 | PIDE/protocol_message.scala | 
| 56385 | 68 | PIDE/prover.scala | 
| 52981 | 69 | PIDE/query_operation.scala | 
| 56208 | 70 | PIDE/resources.scala | 
| 56210 | 71 | PIDE/session.scala | 
| 43320 | 72 | PIDE/text.scala | 
| 44698 | 73 | PIDE/xml.scala | 
| 74 | PIDE/yxml.scala | |
| 57647 | 75 | ROOT.scala | 
| 48346 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: 
48276diff
changeset | 76 | System/command_line.scala | 
| 43744 
2c7e1565b4a3
some support to invoke Scala methods under program control;
 wenzelm parents: 
43730diff
changeset | 77 | System/invoke_scala.scala | 
| 43517 | 78 | System/isabelle_charset.scala | 
| 43320 | 79 | System/isabelle_process.scala | 
| 80 | System/isabelle_system.scala | |
| 48365 
d88aefda01c4
basic support for stand-alone options with external string representation;
 wenzelm parents: 
48346diff
changeset | 81 | System/options.scala | 
| 43320 | 82 | System/platform.scala | 
| 56860 | 83 | System/posix_interrupt.scala | 
| 45027 
f459e93a038e
more abstract wrapping of fifos as System_Channel;
 wenzelm parents: 
44698diff
changeset | 84 | System/system_channel.scala | 
| 50203 | 85 | System/utf8.scala | 
| 43320 | 86 | Thy/html.scala | 
| 50707 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
 wenzelm parents: 
50689diff
changeset | 87 | Thy/present.scala | 
| 43320 | 88 | Thy/thy_header.scala | 
| 43651 
511df47bcadc
some support for theory files within Isabelle/Scala session;
 wenzelm parents: 
43600diff
changeset | 89 | Thy/thy_info.scala | 
| 43320 | 90 | Thy/thy_syntax.scala | 
| 58523 | 91 | Tools/bibtex.scala | 
| 57647 | 92 | Tools/build.scala | 
| 93 | Tools/build_console.scala | |
| 94 | Tools/build_doc.scala | |
| 59891 
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
 wenzelm parents: 
59713diff
changeset | 95 | Tools/check_keywords.scala | 
| 56791 | 96 | Tools/check_source.scala | 
| 52444 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
 wenzelm parents: 
52439diff
changeset | 97 | Tools/doc.scala | 
| 50687 | 98 | Tools/main.scala | 
| 50981 | 99 | Tools/ml_statistics.scala | 
| 56864 | 100 | Tools/print_operation.scala | 
| 54730 | 101 | Tools/simplifier_trace.scala | 
| 50980 | 102 | Tools/task_statistics.scala | 
| 58610 | 103 | Tools/update_cartouches.scala | 
| 58872 | 104 | Tools/update_header.scala | 
| 58861 
5ff61774df11
command-line terminator ";" is no longer accepted;
 wenzelm parents: 
58842diff
changeset | 105 | Tools/update_semicolons.scala | 
| 43320 | 106 | library.scala | 
| 43730 
a0ed7bc688b5
lambda terms with XML data representation in Scala;
 wenzelm parents: 
43715diff
changeset | 107 | term.scala | 
| 43779 | 108 | term_xml.scala | 
| 59441 | 109 | "../Tools/Graphview/graph_file.scala" | 
| 59202 | 110 | "../Tools/Graphview/graph_panel.scala" | 
| 59459 | 111 | "../Tools/Graphview/graphview.scala" | 
| 59232 | 112 | "../Tools/Graphview/layout.scala" | 
| 59202 | 113 | "../Tools/Graphview/main_panel.scala" | 
| 59290 | 114 | "../Tools/Graphview/metrics.scala" | 
| 59202 | 115 | "../Tools/Graphview/model.scala" | 
| 59392 | 116 | "../Tools/Graphview/mutator.scala" | 
| 59202 | 117 | "../Tools/Graphview/mutator_dialog.scala" | 
| 118 | "../Tools/Graphview/mutator_event.scala" | |
| 119 | "../Tools/Graphview/popups.scala" | |
| 120 | "../Tools/Graphview/shapes.scala" | |
| 59392 | 121 | "../Tools/Graphview/tree_panel.scala" | 
| 43320 | 122 | ) | 
| 123 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 124 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 125 | ## diagnostics | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 126 | |
| 43280 | 127 | PRG="$(basename "$0")" | 
| 128 | ||
| 129 | function usage() | |
| 130 | {
 | |
| 131 | echo | |
| 132 | echo "Usage: isabelle $PRG [OPTIONS]" | |
| 133 | echo | |
| 134 | echo " Options are:" | |
| 135 | echo " -f fresh build" | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 136 | echo " -t test separate compilation of PIDE" | 
| 43280 | 137 | echo | 
| 138 | exit 1 | |
| 139 | } | |
| 140 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 141 | function fail() | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 142 | {
 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 143 | echo "$1" >&2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 144 | exit 2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 145 | } | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 146 | |
| 42899 | 147 | [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 148 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 149 | |
| 43280 | 150 | ## process command line | 
| 151 | ||
| 152 | # options | |
| 153 | ||
| 154 | FRESH="" | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 155 | TEST_PIDE="" | 
| 43280 | 156 | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 157 | while getopts "ft" OPT | 
| 43280 | 158 | do | 
| 159 | case "$OPT" in | |
| 160 | f) | |
| 161 | FRESH=true | |
| 162 | ;; | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 163 | t) | 
| 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 164 | TEST_PIDE=true | 
| 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 165 | ;; | 
| 43280 | 166 | \?) | 
| 167 | usage | |
| 168 | ;; | |
| 169 | esac | |
| 170 | done | |
| 171 | ||
| 172 | shift $(($OPTIND - 1)) | |
| 173 | ||
| 174 | ||
| 175 | # args | |
| 176 | ||
| 177 | [ "$#" -ne 0 ] && usage | |
| 178 | ||
| 179 | ||
| 49558 | 180 | ## build | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 181 | |
| 34284 | 182 | TARGET_DIR="$ISABELLE_HOME/lib/classes" | 
| 53577 | 183 | TARGET="$TARGET_DIR/Pure.jar" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 184 | |
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 185 | declare -a PIDE_SOURCES=() | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 186 | declare -a PURE_SOURCES=() | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 187 | |
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 188 | for DEP in "${SOURCES[@]}"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 189 | do | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 190 | if grep "Module:.*PIDE" "$DEP" >/dev/null | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 191 | then | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 192 |     PIDE_SOURCES["${#PIDE_SOURCES[@]}"]="$DEP"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 193 | else | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 194 |     PURE_SOURCES["${#PURE_SOURCES[@]}"]="$DEP"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 195 | fi | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 196 | done | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 197 | |
| 43405 | 198 | declare -a UPDATED=() | 
| 199 | ||
| 43280 | 200 | if [ -n "$FRESH" ]; then | 
| 201 | OUTDATED=true | |
| 202 | else | |
| 203 | OUTDATED=false | |
| 43523 | 204 | if [ ! -e "$TARGET" ]; then | 
| 205 | OUTDATED=true | |
| 206 | else | |
| 43405 | 207 |     for DEP in "${SOURCES[@]}"
 | 
| 43280 | 208 | do | 
| 43405 | 209 | [ ! -e "$DEP" ] && fail "Missing file: $DEP" | 
| 43523 | 210 |       [ "$DEP" -nt "$TARGET" ] && {
 | 
| 211 | OUTDATED=true | |
| 212 |         UPDATED["${#UPDATED[@]}"]="$DEP"
 | |
| 213 | } | |
| 43280 | 214 | done | 
| 43405 | 215 | fi | 
| 43280 | 216 | fi | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 217 | |
| 34284 | 218 | if [ "$OUTDATED" = true ] | 
| 219 | then | |
| 49173 
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
 wenzelm parents: 
49068diff
changeset | 220 | echo "### Building Isabelle/Scala ..." | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 221 | |
| 43405 | 222 |   [ "${#UPDATED[@]}" -gt 0 ] && {
 | 
| 223 | echo "Changed files:" | |
| 224 |     for FILE in "${UPDATED[@]}"
 | |
| 225 | do | |
| 226 | echo " $FILE" | |
| 227 | done | |
| 228 | } | |
| 229 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 230 | rm -rf classes && mkdir classes | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 231 | |
| 47009 | 232 | SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 233 | |
| 50689 | 234 | ( | 
| 58791 | 235 | classpath "$JAVA_HOME/lib/jfxrt.jar" | 
| 53576 
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
 wenzelm parents: 
53519diff
changeset | 236 | classpath classes | 
| 
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
 wenzelm parents: 
53519diff
changeset | 237 | export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")" | 
| 50689 | 238 | |
| 239 | if [ "$TEST_PIDE" = true ]; then | |
| 240 |       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
 | |
| 241 | fail "Failed to compile PIDE sources" | |
| 242 |       isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
 | |
| 243 | fail "Failed to compile Pure sources" | |
| 244 | else | |
| 245 |       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
 | |
| 246 | fail "Failed to compile sources" | |
| 247 | fi | |
| 51508 | 248 | ) || exit "$?" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 249 | |
| 53577 | 250 | mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR" | 
| 43280 | 251 | |
| 43285 | 252 | pushd classes >/dev/null | 
| 43280 | 253 | |
| 43517 | 254 | CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" | 
| 255 | mkdir -p "$(dirname "$CHARSET_SERVICE")" | |
| 256 | echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" | |
| 257 | ||
| 54676 
6b2ca4850b71
uniform use of transparent icons, as for main "apps";
 wenzelm parents: 
54671diff
changeset | 258 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/. | 
| 54709 | 259 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/. | 
| 53452 
8181bc357dc4
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
 wenzelm parents: 
53279diff
changeset | 260 | |
| 53841 | 261 | isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \ | 
| 43523 | 262 | fail "Failed to produce $TARGET" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 263 | |
| 43280 | 264 | popd >/dev/null | 
| 265 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 266 | rm -rf classes | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 267 | fi |