# Magma options file.
#
# Magma copied this file here when it made this directory, so that the settings
# are easily seen: uncomment whatever you want to change.
#
# Everything below is commented out and shows the built-in DEFAULT, so as it
# stands the file changes nothing, and deleting it changes nothing either.
# (The master copy is libs/auxiliary/options in the Magma distribution;
# copy that to $MAGMA_CONFIG_DIR/options if you keep your directory
# somewhere else.)
#
#
# FORMAT
#
#   name <white space> value
#
# The value runs to the end of the line, so it may contain spaces (as a date
# format or an editor command generally will).  Blank lines and lines whose
# first non-blank character is '#' are ignored.  Names are matched without
# regard to case, and if an option is named twice the last line wins.
#
# An unknown name, or a value that makes no sense, warns at startup; a value
# that is merely out of range is quietly brought into range.  Only interactive
# sessions read this file, so a mistake in it can never disturb a script.
#
# See the History Files section of the handbook for the full account:
# https://docs.magma-maths.org/MagmaLanguage/EnvironmentAndOptions/history-files.html

#-------------------------------------------------------------------------
# The history file itself
#-------------------------------------------------------------------------

# Whether to keep a history file at all.  Magma keeps one by default: the
# commands you type are remembered across sessions, so the up arrow in a new
# session reaches what you typed in the last.  Turning it off stops all of it
# -- nothing is written, nothing is read, and the up arrow reaches only the
# current session, as it did before any of this existed.
#
# This line can only be read once the directory holding this file exists;
# if you do not want Magma writing in your home directory at all, set the
# environment variable MAGMA_NO_HISTORY before running Magma.
#history		yes

# How many lines the history file keeps.  It holds the last N lines you have
# typed, whatever sessions they came from, and that is what is loaded into the
# recall buffer when Magma starts.  Zero means no limit: nothing is ever
# discarded from the file.
#
# The file is allowed to drift past N and is trimmed back at a later startup,
# rather than being rewritten every time Magma exits -- so it may hold up to
# twice this number between trims, though only the last N are ever loaded.
#
# Keep it below the recall buffer (SetHistorySize, 2000 lines by default), or
# the preload fills the buffer before you have typed anything and each line you
# type pushes out one that was read.  What is recalled is the last N lines or
# as many as the buffer holds, whichever is fewer; a setting larger than the
# buffer is not refused -- the file is yours to keep as long as you like -- but
# Magma says so, at the start of each session and whenever SetHistorySize
# (in your startup file too) leaves the buffer smaller than this.
#history-lines		1000

# How many lines a printing command shows when it is given `all' with no count
# of its own -- %h, %PA, %p all, and the seed forms.  Zero means no limit.
#
# It is here so that a full history is not emptied onto the screen by accident.
# The command says when it has shortened itself, and a count, or 0, still asks
# for the lot: `%h 20' is the last twenty and `%h 0' is all of them.
#
# It does not touch %e or %E: editing a part of what you asked for would be a
# worse thing than showing you a part of it.
#history-print-lines	100

# Whether to keep the saved/ archive: one file per session, kept for good,
# which is what the session browser browses and what %b, the 'c' and 's' keys
# and the saved-max-* settings below are all about.  Without it you still have
# the history file and the up arrow; you simply have no per-session record.
#
# It is kept if the archive directory already exists, and not otherwise, so
# nobody who has one loses it and nobody else acquires one uninvited.  Say yes
# here to ask for it (or make the directory yourself); the browser also offers
# to turn it on the first time you ask for it and there is nothing to browse.
#
# TURNING IT OFF NEVER DELETES ANYTHING.  An archive you have already is left
# exactly as it is; Magma just stops adding to it, and turning it back on
# resumes.
#
# Unlike most settings, its line below does not show the default, since the
# default depends on the directory: uncomment it to turn the archive on.
# (Simply opening the browser and answering yes also turns it on.)
#saved-sessions		yes


#-------------------------------------------------------------------------
# The browser preview: how much of a session to show
#-------------------------------------------------------------------------

# Lines of each session shown above and below the ellipsis.  A plain number is
# a count of lines; N% is a percentage of the terminal height, worked out
# afresh each time the display is drawn, so it follows the window if you resize
# it while the browser is open.
#
# Percentages truncate: 15% is 3 lines on a 24-row terminal (the same as the
# default) and 7 on a 50-row one, whereas 10% would be only 2 at 24 rows.  At
# least one line is always shown either side, and if the two together would not
# leave the block room on the screen they are reduced until they do.  A session
# short enough to fit in the preview is shown whole, with no ellipsis.
#browser-lines-top	3
#browser-lines-bottom	3


#-------------------------------------------------------------------------
# Browser behaviour
#-------------------------------------------------------------------------

# Ask before 'd' deletes a file.  yes/no, true/false, on/off, 1/0.
#
# Note that 'd' ALWAYS asks when you are browsing a directory other than the
# saved/ archive (see the 'c' key), whatever this says: there the files are
# your own rather than Magma's.
#browser-confirm-delete	yes

# Start matching case-insensitive, for the '&' filter and the '/' and '?'
# searches alike.  The 'i' key still toggles it from there; this is only the
# state each browse begins in.  It applies to regular expressions too (both the
# pattern and the line are folded to lower case).
#browser-filter-ignore-case	no

# Take the pattern typed at the '&', '/' and '?' prompts as a LITERAL string
# rather than a regular expression.  TAB at the prompt switches between the two
# whatever this says, and the prompt shows which is in force ("&re" or "&lit");
# this is only the kind each prompt starts out expecting.
#browser-search-literal		no


#-------------------------------------------------------------------------
# Keys
#-------------------------------------------------------------------------

# Which key opens the session browser, and which starts the incremental
# history search (Ctrl-R in emacs mode: search back through the history for a
# line containing what you type).
#
# A key is written  ^X, C-x or ctrl-x  for a control character, or
# esc-x, M-x or meta-x  for Esc followed by x; "none" leaves it unbound.  The
# letter is not case-sensitive.
#
# Neither search key may be an Esc-x key, and no key may be Backspace, Tab,
# Return or Esc (^H, ^I, ^J, ^M, ^[).
#
# In VI mode Ctrl-R on an empty line opens the browser (or, with no archive
# kept, offers to start one), and the search is on / in command mode, as in
# readline and ksh: Esc there means "enter command mode", so a meta key cannot
# work, and Ctrl-R is wanted for the browser.  search-key-vi may be / or ?,
# which work in command mode only; within that search Ctrl-P steps back to the
# next older match.  It may also be a control key, which then does that
# itself.  In EMACS mode
# Ctrl-R is the search -- the readline and IPython convention -- and the
# browser moves to Esc-r, which is the only portable choice left: of the
# control keys still free, ^S and ^Q are flow control, ^Z suspends, and ^O and
# ^T are the discard and status characters on macOS and the BSDs, so they
# would work here and silently do nothing on a colleague's Mac.  A second
# Ctrl-R at an empty search prompt also opens the browser, and %b opens it
# whatever these say.
#browser-key-emacs		esc-r
#browser-key-vi			^R
#search-key			^R
#search-key-vi			/

# Ignore case in the Ctrl-R and / search.  (Off, as browser-filter-ignore-case
# is.)
#search-ignore-case		no

# Editor for the 'E' and 'e' keys; may include arguments, and the file name is
# appended.  Unset means $EDITOR, then /bin/ed.  Worth setting only if you want
# history editing to use a different editor from everything else.
#
# The built-in default is unset, so the line below does not show it.  The
# command is run by the shell, so uncommenting the line as it stands uses
# $EDITOR, but without the fall-back to /bin/ed when EDITOR is not set.
#browser-editor		$EDITOR


#-------------------------------------------------------------------------
# Browser appearance
#-------------------------------------------------------------------------

# Box colour: blue, cyan, green, red, magenta, yellow, white, or none (the last
# draws the box without colour).  "browser-colour" is the same option.
#browser-color		blue

# Plain, unboxed, uncoloured display: no, yes, or dumb.
#
# "dumb" is plain and, in addition, emits no terminal escape sequence at all --
# not even the cursor movement the browser repaints itself with, so each
# keystroke prints a fresh block below the last one and the screen scrolls.  It
# is for a terminal that does not understand the usual sequences, and is chosen
# automatically when TERM is unset or is "dumb".
#
# Setting the environment variable MAGMA_HIST_PLAIN forces this for a single
# session without editing this file (MAGMA_HIST_PLAIN=dumb asks for the dumb
# level); note that the variable can only make the display plainer, never
# fancier.
#browser-plain		no

# Tab stop width, 1 to 32, for indentation in the preview.
#browser-tab-width	8

# Date shown in the browser's banner, as a strftime format.  If it yields
# nothing, or is too long to fit, the file name is shown instead.
#
# The default deliberately omits %Z (the time zone: "AEST"), which is the same
# for every session you are ever likely to browse and only eats banner width.
# To put it back:
#	browser-date-format	%a %b %e %H:%M:%S %Z %Y
# Or something shorter, leaving more room for the rest of the banner:
#	browser-date-format	%Y-%m-%d %H:%M
#browser-date-format	%a %b %e %H:%M:%S %Y

# How much of a file's NAME to show in the banner, for files whose name is not
# one of Magma's own and so has to be shown as well as the date (see the 'c'
# key below).  0 means show all of it -- but then a long name can push the
# "(3/12)" position off the right of the box, which is what the limit is for.
#browser-name-max	32


#-------------------------------------------------------------------------
# What gets recorded
#-------------------------------------------------------------------------

# Whether a line consisting of just "quit;" (the command that ends the
# session) is written to the saved file.  On (the default) means it is dropped:
# it merely repeats in every session and is no help on recall.  Turn it off if
# you type code in which a whole physical line is legitimately "quit;" -- for
# instance inside a multi-line string literal -- and want the saved session to
# reproduce it exactly.  Blank lines are always dropped, regardless of this.
#remove-quit		yes


#-------------------------------------------------------------------------
# The saved/ archive  --  NOT browser settings: these DELETE FILES
#-------------------------------------------------------------------------

# The archive otherwise grows for ever, one file per session.  Keep only the
# newest N sessions, and/or only the last N days.  Either may be given, or
# both.  Zero means no limit, which is the default: nothing is ever discarded
# unless you ask for it here.
#
# Applied at startup, before the session's own file is created -- so that file
# can never be deleted by them, and the directory holds one more than
# saved-max-files says until the next start trims it back.  Only files named as
# Magma names them are considered, so anything else you keep in saved/ is safe,
# and a file another Magma is still writing to is left alone however old it is.
#
# Worth remembering before setting these: saved/ is the real archive of your
# work -- the history file holds only the last history-lines lines, mixed
# together in the order you typed them, and keeps no record of which session
# was which.  The reason you might still want a limit is that the '/' and '?'
# filters read every file in the archive in order to match it.
#
# These two settings mean nothing with saved-sessions off: there is no archive
# for them to trim.
#saved-max-files	0
#saved-max-days		0


#-------------------------------------------------------------------------
# Note: browsing somewhere other than saved/  (no option needed)
#-------------------------------------------------------------------------
#
# The 'c' key in the browser prompts for a directory and browses that instead
# of the saved/ archive -- typically wherever you have been putting sessions
# with the 's' key.  An empty answer returns you to saved/.  At that prompt (and
# the 's' save prompt) TAB completes the name, the left/right arrows and the
# usual control keys edit it (Ctrl-A/E, Ctrl-B/F, Ctrl-D, Ctrl-K, Ctrl-W,
# Ctrl-U), and Esc abandons it.
#
# In such a directory every plain file is listed (names there mean nothing to
# Magma), ordered by modification time, newest first; the banner shows that
# time and then the file's name -- which is itself how you can tell you are not
# in the saved/ archive, where only the date is shown.  Everything else --
# Return/r to run, Space to load, the filters, E/e, s -- works as it does in
# saved/, except that 'd' always asks for confirmation.
