src/Tools/jEdit/lib/Tools/jedit
author wenzelm
Mon, 10 May 2021 22:18:12 +0200
changeset 73660 ff716ecb0805
parent 73653 d9823224fcfe
child 73661 8b3e672df28c
permissions -rwxr-xr-x
put more resources into jedit_build component;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
     2
#
34664
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
     3
# Author: Makarius
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
     4
#
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
     5
# DESCRIPTION: Isabelle/jEdit interface wrapper
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
     6
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
     7
## sources
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
     8
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
     9
declare -a SOURCES0=(
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    10
  "src/Tools/jEdit/src-base/dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    11
  "src/Tools/jEdit/src-base/isabelle_encoding.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    12
  "src/Tools/jEdit/src-base/jedit_lib.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    13
  "src/Tools/jEdit/src-base/pide_docking_framework.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    14
  "src/Tools/jEdit/src-base/plugin.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    15
  "src/Tools/jEdit/src-base/syntax_style.scala"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
    16
)
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
    17
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    18
declare -a RESOURCES0=(
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    19
  "src/Tools/jEdit/src-base/Isabelle_Base.props"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    20
  "src/Tools/jEdit/src-base/services.xml"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
    21
)
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
    22
43320
wenzelm
parents: 43287
diff changeset
    23
declare -a SOURCES=(
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    24
  "src/Tools/jEdit/src/active.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    25
  "src/Tools/jEdit/src/completion_popup.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    26
  "src/Tools/jEdit/src/context_menu.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    27
  "src/Tools/jEdit/src/debugger_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    28
  "src/Tools/jEdit/src/document_model.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    29
  "src/Tools/jEdit/src/document_view.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    30
  "src/Tools/jEdit/src/documentation_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    31
  "src/Tools/jEdit/src/fold_handling.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    32
  "src/Tools/jEdit/src/font_info.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    33
  "src/Tools/jEdit/src/graphview_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    34
  "src/Tools/jEdit/src/info_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    35
  "src/Tools/jEdit/src/isabelle.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    36
  "src/Tools/jEdit/src/isabelle_encoding.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    37
  "src/Tools/jEdit/src/isabelle_export.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    38
  "src/Tools/jEdit/src/isabelle_options.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    39
  "src/Tools/jEdit/src/isabelle_session.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    40
  "src/Tools/jEdit/src/isabelle_sidekick.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    41
  "src/Tools/jEdit/src/isabelle_vfs.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    42
  "src/Tools/jEdit/src/jedit_bibtex.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    43
  "src/Tools/jEdit/src/jedit_editor.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    44
  "src/Tools/jEdit/src/jedit_lib.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    45
  "src/Tools/jEdit/src/jedit_options.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    46
  "src/Tools/jEdit/src/jedit_rendering.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    47
  "src/Tools/jEdit/src/jedit_resources.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    48
  "src/Tools/jEdit/src/jedit_sessions.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    49
  "src/Tools/jEdit/src/jedit_spell_checker.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    50
  "src/Tools/jEdit/src/keymap_merge.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    51
  "src/Tools/jEdit/src/monitor_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    52
  "src/Tools/jEdit/src/output_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    53
  "src/Tools/jEdit/src/plugin.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    54
  "src/Tools/jEdit/src/pretty_text_area.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    55
  "src/Tools/jEdit/src/pretty_tooltip.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    56
  "src/Tools/jEdit/src/process_indicator.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    57
  "src/Tools/jEdit/src/protocol_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    58
  "src/Tools/jEdit/src/query_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    59
  "src/Tools/jEdit/src/raw_output_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    60
  "src/Tools/jEdit/src/rich_text_area.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    61
  "src/Tools/jEdit/src/scala_console.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    62
  "src/Tools/jEdit/src/session_build.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    63
  "src/Tools/jEdit/src/simplifier_trace_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    64
  "src/Tools/jEdit/src/simplifier_trace_window.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    65
  "src/Tools/jEdit/src/sledgehammer_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    66
  "src/Tools/jEdit/src/state_dockable.scala"
72248
71378e7d148e clarified modules;
wenzelm
parents: 72247
diff changeset
    67
  "src/Tools/jEdit/src/status_widget.scala"
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    68
  "src/Tools/jEdit/src/symbols_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    69
  "src/Tools/jEdit/src/syntax_style.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    70
  "src/Tools/jEdit/src/syslog_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    71
  "src/Tools/jEdit/src/text_overview.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    72
  "src/Tools/jEdit/src/text_structure.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    73
  "src/Tools/jEdit/src/theories_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    74
  "src/Tools/jEdit/src/timing_dockable.scala"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    75
  "src/Tools/jEdit/src/token_markup.scala"
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
    76
)
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
    77
43320
wenzelm
parents: 43287
diff changeset
    78
declare -a RESOURCES=(
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    79
  "src/Tools/jEdit/src/actions.xml"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    80
  "src/Tools/jEdit/src/dockables.xml"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    81
  "src/Tools/jEdit/src/Isabelle.props"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
    82
  "src/Tools/jEdit/src/services.xml"
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
    83
)
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
    84
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
    85
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    86
## diagnostics
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    87
34664
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
    88
PRG="$(basename "$0")"
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
    89
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
    90
function usage()
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    91
{
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    92
  echo
34664
8f5fbe4a80ff Isabelle component;
wenzelm
parents: 34663
diff changeset
    93
  echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    94
  echo
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
    95
  echo "  Options are:"
71548
e32255318cb2 proper usage (amending 8c7706b053c7);
wenzelm
parents: 71375
diff changeset
    96
  echo "    -A NAME      ancestor session for option -R (default: parent)"
62039
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 61512
diff changeset
    97
  echo "    -D NAME=X    set JVM system property"
66683
01189e46dc55 misc tuning and updates for release;
wenzelm
parents: 66591
diff changeset
    98
  echo "    -J OPTION    add JVM runtime option"
01189e46dc55 misc tuning and updates for release;
wenzelm
parents: 66591
diff changeset
    99
  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 67992
diff changeset
   100
  echo "    -R NAME      build image with requirements from other sessions"
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   101
  echo "    -b           build only"
48791
9e8f30bfbdca added jedit option -d;
wenzelm
parents: 48603
diff changeset
   102
  echo "    -d DIR       include session directory"
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   103
  echo "    -f           fresh build"
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   104
  echo "    -i NAME      include session in name-space of theories"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   105
  echo "    -j OPTION    add jEdit runtime option"
66683
01189e46dc55 misc tuning and updates for release;
wenzelm
parents: 66591
diff changeset
   106
  echo "                 (default $JEDIT_OPTIONS)"
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50373
diff changeset
   107
  echo "    -l NAME      logic session name"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   108
  echo "    -m MODE      add print mode for output"
57086
wenzelm
parents: 57032
diff changeset
   109
  echo "    -n           no build of session image on startup"
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   110
  echo "    -p CMD       ML process command prefix (process policy)"
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   111
  echo "    -s           system build mode for session image (system_heaps=true)"
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   112
  echo "    -u           user build mode for session image (system_heaps=false)"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   113
  echo
61171
2a56a53d78f9 tuned message;
wenzelm
parents: 61133
diff changeset
   114
  echo "  Start jEdit with Isabelle plugin setup and open FILES"
61512
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61511
diff changeset
   115
  echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   116
  echo
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   117
  exit 1
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   118
}
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   119
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   120
function fail()
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   121
{
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   122
  echo "$1" >&2
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   123
  exit 2
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   124
}
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   125
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   126
function failed()
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   127
{
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   128
  fail "Failed!"
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   129
}
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   130
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   131
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   132
## process command line
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   133
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   134
# options
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   135
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   136
BUILD_ONLY=false
71372
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   137
FRESH_BUILD=""
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   138
ML_PROCESS_POLICY=""
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   139
JEDIT_LOGIC_ANCESTOR=""
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 67992
diff changeset
   140
JEDIT_LOGIC_REQUIREMENTS=""
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   141
JEDIT_INCLUDE_SESSIONS=""
70382
23ba5a638e6d more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents: 70220
diff changeset
   142
JEDIT_SESSION_DIRS="-"
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50373
diff changeset
   143
JEDIT_LOGIC=""
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   144
JEDIT_PRINT_MODE=""
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   145
JEDIT_NO_BUILD=""
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   146
JEDIT_BUILD_MODE="default"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   147
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   148
function getoptions()
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   149
{
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   150
  OPTIND=1
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70382
diff changeset
   151
  while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   152
  do
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   153
    case "$OPT" in
66988
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   154
      A)
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   155
        JEDIT_LOGIC_ANCESTOR="$OPTARG"
7f8c1dd7576a support alternative ancestor session;
wenzelm
parents: 66987
diff changeset
   156
        ;;
62039
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 61512
diff changeset
   157
      D)
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 61512
diff changeset
   158
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 61512
diff changeset
   159
        ;;
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   160
      J)
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   161
        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   162
        ;;
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63987
diff changeset
   163
      R)
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 67992
diff changeset
   164
        JEDIT_LOGIC="$OPTARG"
bcdc47c9d4af clarified signature;
wenzelm
parents: 67992
diff changeset
   165
        JEDIT_LOGIC_REQUIREMENTS="true"
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63987
diff changeset
   166
        ;;
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   167
      b)
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   168
        BUILD_ONLY=true
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   169
        ;;
48791
9e8f30bfbdca added jedit option -d;
wenzelm
parents: 48603
diff changeset
   170
      d)
70382
23ba5a638e6d more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents: 70220
diff changeset
   171
        JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
48791
9e8f30bfbdca added jedit option -d;
wenzelm
parents: 48603
diff changeset
   172
        ;;
68541
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   173
      i)
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   174
        if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   175
          JEDIT_INCLUDE_SESSIONS="$OPTARG"
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   176
        else
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   177
          JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   178
        fi
12b4b3bc585d command-line option for include_sessions;
wenzelm
parents: 68370
diff changeset
   179
        ;;
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   180
      f)
71372
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   181
        FRESH_BUILD="true"
43285
966f359dc724 further jedit build option;
wenzelm
parents: 43284
diff changeset
   182
        ;;
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   183
      j)
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   184
        ARGS["${#ARGS[@]}"]="$OPTARG"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   185
        ;;
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   186
      l)
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   187
        JEDIT_LOGIC="$OPTARG"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   188
        ;;
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   189
      m)
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   190
        if [ -z "$JEDIT_PRINT_MODE" ]; then
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   191
          JEDIT_PRINT_MODE="$OPTARG"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   192
        else
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   193
          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   194
        fi
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   195
        ;;
50405
366c4a602500 clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents: 50403
diff changeset
   196
      n)
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   197
        JEDIT_NO_BUILD="true"
50405
366c4a602500 clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
wenzelm
parents: 50403
diff changeset
   198
        ;;
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   199
      p)
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   200
        ML_PROCESS_POLICY="$OPTARG"
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   201
        ;;
50373
025f758fa24b implicit build_dialog for Isabelle/jEdit;
wenzelm
parents: 50306
diff changeset
   202
      s)
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53446
diff changeset
   203
        JEDIT_BUILD_MODE="system"
50373
025f758fa24b implicit build_dialog for Isabelle/jEdit;
wenzelm
parents: 50306
diff changeset
   204
        ;;
69854
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   205
      u)
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   206
        JEDIT_BUILD_MODE="user"
cc0b3e177b49 system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents: 69762
diff changeset
   207
        ;;
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   208
      \?)
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   209
        usage
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   210
        ;;
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   211
    esac
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   212
  done
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   213
}
34581
abab3a577e10 slightly more robust treatment of options via arrays;
wenzelm
parents: 34412
diff changeset
   214
66906
03a96b8c7c06 updated to jdk-8u152, which is for x86_64 only;
wenzelm
parents: 66683
diff changeset
   215
eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
34843
eb8806a2e348 define scala.home, for more robust startup of Scala tools, notably the compiler;
wenzelm
parents: 34790
diff changeset
   216
53446
4adb2cce5fc6 use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
wenzelm
parents: 53445
diff changeset
   217
declare -a ARGS=()
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   218
34780
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   219
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   220
getoptions "${OPTIONS[@]}"
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   221
d0ff1c3a91ea more serious command line handling;
wenzelm
parents: 34691
diff changeset
   222
getoptions "$@"
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   223
shift $(($OPTIND - 1))
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   224
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   225
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   226
# args
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   227
61512
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61511
diff changeset
   228
while [ "$#" -gt 0 ]; do
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61511
diff changeset
   229
  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61511
diff changeset
   230
  shift
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61511
diff changeset
   231
done
34333
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   232
b353b4cd9bd4 Isabelle/jEdit interface wrapper.
wenzelm
parents:
diff changeset
   233
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   234
## dependencies
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   235
49953
fc2e3b9d4852 avoid duplicate build of jars_fresh;
wenzelm
parents: 49726
diff changeset
   236
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
62589
b5783412bfed prefer plain "isabelle" from PATH within Isabelle settings environment;
wenzelm
parents: 62039
diff changeset
   237
  isabelle browser -b || exit $?
71372
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   238
  if [ -n "$FRESH_BUILD" ]; then
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   239
    "$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   240
  else
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   241
    "$ISABELLE_HOME/Admin/build" jars || exit $?
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   242
  fi
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   243
elif [ -n "$FRESH_BUILD" ]; then
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   244
  echo >&2 "### Ignoring fresh build option: not a repository clone"
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   245
  FRESH_BUILD=""
49953
fc2e3b9d4852 avoid duplicate build of jars_fresh;
wenzelm
parents: 49726
diff changeset
   246
fi
43413
7a7604573ecd explicit dependency on Pure.jar;
wenzelm
parents: 43405
diff changeset
   247
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   248
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   249
# target
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   250
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   251
pushd "$ISABELLE_HOME" >/dev/null || failed
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   252
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   253
TARGET_DIR="src/Tools/jEdit/dist"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   254
TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   255
TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   256
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   257
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   258
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
73653
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 73652
diff changeset
   259
for DEP in "$TARGET_DIR"/jars/*.jar
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   260
do
73653
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 73652
diff changeset
   261
  TARGET_DEPS["${#TARGET_DEPS[@]}"]="$DEP"
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   262
done
43384
9c228b8953f2 more explicit check of dependencies;
wenzelm
parents: 43381
diff changeset
   263
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   264
function target_shasum()
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   265
(
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   266
  shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   267
    "${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   268
)
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   269
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   270
function target_clean()
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   271
{
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   272
  rm -rf "$ISABELLE_HOME/$TARGET_DIR"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   273
}
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   274
71372
85274743f789 clarified option -f: avoid accidental target_clean for proper release snapshot;
wenzelm
parents: 71371
diff changeset
   275
[ -n "$FRESH_BUILD" ] && target_clean
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   276
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   277
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   278
## build
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   279
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   280
BUILD_DIR="$TARGET_DIR/build"
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   281
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   282
function init_resources ()
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   283
{
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   284
  mkdir -p "$BUILD_DIR" || failed
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   285
  cp -p -R "$@" "$BUILD_DIR/."
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   286
}
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   287
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   288
function compile_sources()
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   289
{
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   290
  (
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   291
    #FIXME workarounds for scalac 2.11.0
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   292
    export CYGWIN="nodosfilewarning"
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   293
    function stty() { :; }
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   294
    export -f stty
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   295
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   296
    for DEP in "${TARGET_DEPS[@]}"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   297
    do
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   298
      classpath "$DEP"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   299
    done
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   300
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   301
    isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   302
  ) || fail "Failed to compile sources"
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   303
}
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   304
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   305
function make_jar()
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   306
{
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   307
  isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   308
  rm -rf "$ISABELLE_HOME/$BUILD_DIR"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   309
}
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   310
71375
5ccf60c1f47c tuned messages;
wenzelm
parents: 71372
diff changeset
   311
target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
71371
1c4ec697bee5 more robust;
wenzelm
parents: 71368
diff changeset
   312
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
43405
723a8af9d3f0 tuned messages;
wenzelm
parents: 43395
diff changeset
   313
  echo "### Building Isabelle/jEdit ..."
723a8af9d3f0 tuned messages;
wenzelm
parents: 43395
diff changeset
   314
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   315
  [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   316
    fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   317
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   318
  target_clean || failed
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   319
  mkdir -p "$TARGET_DIR" || failed
43287
acc680ab6204 simplified directory structure;
wenzelm
parents: 43286
diff changeset
   320
73653
d9823224fcfe build auxiliary jEdit component in Isabelle/Scala;
wenzelm
parents: 73652
diff changeset
   321
  cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   322
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   323
  init_resources "${RESOURCES0[@]}"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   324
  compile_sources "${SOURCES0[@]}"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   325
  make_jar "$TARGET_JAR0"
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   326
  classpath "$TARGET_JAR0"
66457
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   327
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   328
  init_resources "${RESOURCES[@]}"
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin;
wenzelm
parents: 66120
diff changeset
   329
  compile_sources "${SOURCES[@]}"
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   330
  make_jar "$TARGET_JAR"
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56421
diff changeset
   331
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   332
  target_shasum > "$TARGET_SHASUM"
43284
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   333
fi
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   334
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   335
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   336
## main
04d473e883df build jedit as part of regular startup script (in that case depending on jedit_build component);
wenzelm
parents: 41380
diff changeset
   337
71368
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   338
popd >/dev/null
fd5cd1daf6a9 build in $ISABELLE_HOME;
wenzelm
parents: 70683
diff changeset
   339
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: 53451
diff changeset
   340
if [ "$BUILD_ONLY" = false ]
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: 53451
diff changeset
   341
then
73161
31fbde3baa97 more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents: 72248
diff changeset
   342
  "$ISABELLE_HOME/lib/scripts/java-gui-setup"
31fbde3baa97 more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
wenzelm
parents: 72248
diff changeset
   343
68370
bcdc47c9d4af clarified signature;
wenzelm
parents: 67992
diff changeset
   344
  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
70683
8c7706b053c7 find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents: 70382
diff changeset
   345
    JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 63734
diff changeset
   346
  export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
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: 53451
diff changeset
   347
  classpath "$JEDIT_HOME/dist/jedit.jar"
70220
089753519be0 more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
wenzelm
parents: 69854
diff changeset
   348
  exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
089753519be0 more uniform Isabelle splash screen -- avoid problems with jEdit splash and Java 11 on some Linux window managers;
wenzelm
parents: 69854
diff changeset
   349
    "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
50416
2e1b47e22fc6 more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;
wenzelm
parents: 50405
diff changeset
   350
fi