History log of /seL4-l4v-master/HOL4/tools/Holmake/internal_functions.sml
Revision Date Author Comments
# b03aecf7 16-May-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Read Holmakefiles fewer times, speeding up startup times

This speeds up Holmake, hol and script files.

Also remove output of loadPath deltas as hol starts.


# 28701945 16-May-2019 Michael Norrish <michael.norrish@nicta.com.au>

Make Holmake's internal_functions' find_unescaped more efficient

Profiling showed this function taking rather longer than one would
want.


# acd07026 22-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix Holmake's wildcard fn to interpret arg as multiple patterns

So, $(wildcard foo* bar*) now searches current directory for files
beginning with foo, and those beginning with bar. Previously, the
space would have been interpreted as a literal space. To get the
literal space, you need to escape it with a backslash (as per the 8th
testcase in the regression test directory).


# b232e939 22-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix Holmake's $(wildcard ...) fn to return "" when matches fail

This is consistent with documentation at

https://www.gnu.org/software/make/manual/html_node/Wildcard-Function.html

except that suggests you can have multiple wildcard patterns rather
than just one. (Just noticed this!)

Thanks to Magnus for discussion leading to fix.


# 14729cb1 26-Nov-2017 Oskar Abrahamsson <oskar8192@gmail.com>

Replace "failure" message with an empty string


# f1a8321b 26-Nov-2017 Oskar Abrahamsson <oskar8192@gmail.com>

Remove carriage returns from input


# 968495c6 25-Nov-2017 Oskar Abrahamsson <oskar8192@gmail.com>

Add support for 'shell' in Holmake


# 13060d5b 03-Aug-2015 Michael Norrish <Michael.Norrish@nicta.com.au>

Implement & document which fn for Holmakefiles


# 4a96c6ad 27-Oct-2014 Michael Norrish <michael.norrish@nicta.com.au>

Implement wildcard function for Holmake.

Closes #36


# 0220ddfd 30-Mar-2010 Michael Norrish <Michael.Norrish@nicta.com.au>

Add new findstring function to Holmake language (copying GNU make).


# 7154aa49 31-Jul-2009 Michael Norrish <Michael.Norrish@nicta.com.au>

Start to implement the Basis 97 extensions that Moscow ML hasn't got
in order to force our codebase to get up-to-date. It should also
mean less bodging around for the Poly/ML code. I haven't checked that
my changes to tools-poly/poly/poly-init2.ML have done all that is
required yet. Feel free to fix problems arising there (I hope it will
just be a matter of deleting things).


# 32006915 25-Aug-2006 Michael Norrish <Michael.Norrish@nicta.com.au>

Introduce new makefile function called dprot for quoting file-names that
may include spaces and which need to be mentioned as dependencies in
Holmakefiles. Document its existence in the Description. Tighten up
some of the text-processing done inside Holmakefiles.


# af709bc9 02-Jul-2003 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix for a problem Konrad identified with the way that Holmake was protecting
its built-in variables (MOSMLCOMP etc). Now Holmake doesn't protect
variables that may be used in situations where they are concatenated
with others, but does protect those that will be used on their own (such
as MOSMLC etc).
This requires the provision of a protect function in make-files, so
this is documented in the DESCRIPTION. I think things should be right,
but please check that this works, particularly anyone on Windows!


# 18a48b81 30-Jan-2003 Michael Norrish <Michael.Norrish@nicta.com.au>

Implement patsubst internal function, and shift some useful code into
a separate file.