more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Cumulative reports for Poly/ML profiling output.
THIS="$(cd $(dirname "$0"); pwd)"
SRC="$1"
DST="$2"
mkdir -p "$DST"
for FILE in "$SRC"/*.gz
do
echo "$FILE"
NAME="$(basename "$FILE" .gz)"
gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
done