SourceFileOpsExtras.mesa
Copyright Ó 1989 by Xerox Corporation. All rights reserved.
Linda Howe October 13, 1989 5:03:21 pm PDT
Coolidge, July 17, 1990 5:17 pm PDT
Christian Jacobi, August 24, 1990 12:35 pm PDT
Last tweaked by Mike Spreitzer on December 11, 1990 7:04 pm PST
Some basic feedback operations on source files. Implemented in the most reasonable way for each world.
DIRECTORY
IO USING [STREAM],
PFS USING [nullUniqueID, UniqueID],
PFSNames USING [PATH],
Rope USING [ROPE],
SourceFileOps USING [Index, PosKind, Range, WhichSelection];
SourceFileOpsExtras: CEDAR DEFINITIONS ~ BEGIN
ROPE: TYPE ~ Rope.ROPE;
Position: TYPE ~ RECORD [
fileName: FileName,
uniqueID: UniqueID,
index: ARRAY PosKind OF Range];
A position in a file may be identified by either or both of a line number range and a character index range. Sloppy people (and programs) can make Positions with uniqueID=nullUniqueID; when interpreting such a position, any file with the given name will do.
FileName: TYPE ~ PFSNames.PATH;
UniqueID: TYPE ~ PFS.UniqueID;
PosKind: TYPE ~ SourceFileOps.PosKind;
Range: TYPE ~ SourceFileOps.Range;
Index: TYPE ~ SourceFileOps.Index;
noPosition: Position ~ [noName, nullUniqueID, ALL[noRange]];
noName: FileName ~ NIL;
noIndex: Index ~ INT.FIRST;
nullUniqueID: UniqueID ~ PFS.nullUniqueID;
noRange: Range ~ [];
WhichSelection: TYPE ~ SourceFileOps.WhichSelection;
Denotes choice of what selection to use.
FullGetSelection: PROC [selection: WhichSelection ← primary] RETURNS [pos: Position, contents: ROPE];
Returns the file name and position within the file for the selected text viewer.
Returns noPosition if no valid editor viewer is selected.
Also returns selection contents (as ROPE).
FullFormatPosition: PROC [Position] RETURNS [ROPE];
FullFmtIdxs: PROC [pos: Position] RETURNS [ROPE];
FmtRange: PROC [r: Range, introSingular, introPlural: ROPENIL] RETURNS [ROPE];
FullOpenSource: ShowProc;
ShowProc: TYPE ~ PROC [desc: ROPE, pos: Position, feedBack: IO.STREAM, selection: WhichSelection ← feedback];
Directs the user's attention to the given position, describing it as desc when text is used.
END.