Skip to content

Commit

Permalink
Added bundled agda
Browse files Browse the repository at this point in the history
  • Loading branch information
markokoleznik committed Oct 12, 2015
1 parent a989bf5 commit d1b4e20
Show file tree
Hide file tree
Showing 25 changed files with 4,572 additions and 20 deletions.
8 changes: 8 additions & 0 deletions Agda Writer.xcodeproj/project.pbxproj
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
objects = {

/* Begin PBXBuildFile section */
D524F8891BCB9CB200785995 /* agda in Resources */ = {isa = PBXBuildFile; fileRef = D524F8881BCB9CB200785995 /* agda */; settings = {ASSET_TAGS = (); }; };
D524F8B01BCBAAAA00785995 /* Agda-2.4.2.2 in Resources */ = {isa = PBXBuildFile; fileRef = D524F8AF1BCBAAAA00785995 /* Agda-2.4.2.2 */; settings = {ASSET_TAGS = (); }; };
D531F1031B55E580002E7E0F /* AppDelegate.m in Sources */ = {isa = PBXBuildFile; fileRef = D531F1021B55E580002E7E0F /* AppDelegate.m */; };
D531F1051B55E580002E7E0F /* main.m in Sources */ = {isa = PBXBuildFile; fileRef = D531F1041B55E580002E7E0F /* main.m */; };
D531F1081B55E580002E7E0F /* ViewController.m in Sources */ = {isa = PBXBuildFile; fileRef = D531F1071B55E580002E7E0F /* ViewController.m */; };
Expand Down Expand Up @@ -70,6 +72,8 @@
/* End PBXContainerItemProxy section */

/* Begin PBXFileReference section */
D524F8881BCB9CB200785995 /* agda */ = {isa = PBXFileReference; lastKnownFileType = "compiled.mach-o.executable"; name = agda; path = agda/agda; sourceTree = "<group>"; };
D524F8AF1BCBAAAA00785995 /* Agda-2.4.2.2 */ = {isa = PBXFileReference; lastKnownFileType = folder; name = "Agda-2.4.2.2"; path = "agda/Agda-2.4.2.2"; sourceTree = "<group>"; };
D531F0FC1B55E580002E7E0F /* Agda Writer.app */ = {isa = PBXFileReference; explicitFileType = wrapper.application; includeInIndex = 0; path = "Agda Writer.app"; sourceTree = BUILT_PRODUCTS_DIR; };
D531F1001B55E580002E7E0F /* Info.plist */ = {isa = PBXFileReference; lastKnownFileType = text.plist.xml; path = Info.plist; sourceTree = "<group>"; };
D531F1011B55E580002E7E0F /* AppDelegate.h */ = {isa = PBXFileReference; lastKnownFileType = sourcecode.c.h; path = AppDelegate.h; sourceTree = "<group>"; };
Expand Down Expand Up @@ -211,6 +215,8 @@
D531F0FF1B55E580002E7E0F /* Supporting Files */ = {
isa = PBXGroup;
children = (
D524F8AF1BCBAAAA00785995 /* Agda-2.4.2.2 */,
D524F8881BCB9CB200785995 /* agda */,
D534F8F91B7383D80009D7B0 /* TODO List */,
D531F1771B5852EE002E7E0F /* defaults.plist */,
D531F1001B55E580002E7E0F /* Info.plist */,
Expand Down Expand Up @@ -529,6 +535,7 @@
isa = PBXResourcesBuildPhase;
buildActionMask = 2147483647;
files = (
D524F8891BCB9CB200785995 /* agda in Resources */,
D538E5D21B5EF13300B5455A /* AWInputViewController.xib in Resources */,
D538E5D41B5FD0F300B5455A /* Key Bindings.plist in Resources */,
D5B327EF1B78B65E00EDFC26 /* check-mark.png in Resources */,
Expand All @@ -538,6 +545,7 @@
D5B327F01B78B65E00EDFC26 /* x-mark.png in Resources */,
D531F1721B57E60B002E7E0F /* failed_default.png in Resources */,
D531F1731B57E60B002E7E0F /* load_failed.png in Resources */,
D524F8B01BCBAAAA00785995 /* Agda-2.4.2.2 in Resources */,
D5ECB1D21B84EC8D0099CE5C /* icon_128x128.png in Resources */,
D531F1751B57E60B002E7E0F /* load_successful.png in Resources */,
D5B327F11B78B65E00EDFC26 /* settings-keybindings.png in Resources */,
Expand Down
Binary file not shown.
Original file line number Diff line number Diff line change
Expand Up @@ -32,11 +32,11 @@
ignoreCount = "0"
continueAfterRunningActions = "No"
filePath = "Agda Writer/AWCommunitacion.m"
timestampString = "461019870.055661"
timestampString = "466336721.831631"
startingColumnNumber = "9223372036854775807"
endingColumnNumber = "9223372036854775807"
startingLineNumber = "306"
endingLineNumber = "306"
startingLineNumber = "321"
endingLineNumber = "321"
landmarkName = "-writeDataToAgda:sender:"
landmarkType = "5">
</BreakpointContent>
Expand Down Expand Up @@ -464,11 +464,11 @@
ignoreCount = "0"
continueAfterRunningActions = "No"
filePath = "Agda Writer/AWCommunitacion.m"
timestampString = "459712451.953828"
timestampString = "466333925.740274"
startingColumnNumber = "9223372036854775807"
endingColumnNumber = "9223372036854775807"
startingLineNumber = "81"
endingLineNumber = "81"
startingLineNumber = "82"
endingLineNumber = "82"
landmarkName = "-dataAvailabe:"
landmarkType = "5">
</BreakpointContent>
Expand Down Expand Up @@ -896,11 +896,11 @@
ignoreCount = "0"
continueAfterRunningActions = "No"
filePath = "Agda Writer/AWCommunitacion.m"
timestampString = "461019830.046375"
timestampString = "466336721.831631"
startingColumnNumber = "9223372036854775807"
endingColumnNumber = "9223372036854775807"
startingLineNumber = "267"
endingLineNumber = "267"
startingLineNumber = "282"
endingLineNumber = "282"
landmarkName = "-handleAgdaResponse:"
landmarkType = "5">
</BreakpointContent>
Expand All @@ -912,11 +912,11 @@
ignoreCount = "0"
continueAfterRunningActions = "No"
filePath = "Agda Writer/AWCommunitacion.m"
timestampString = "461019880.951511"
timestampString = "466336721.831631"
startingColumnNumber = "9223372036854775807"
endingColumnNumber = "9223372036854775807"
startingLineNumber = "273"
endingLineNumber = "273"
startingLineNumber = "288"
endingLineNumber = "288"
landmarkName = "-handleAgdaResponse:"
landmarkType = "5">
</BreakpointContent>
Expand Down
3 changes: 1 addition & 2 deletions Agda Writer/AWCommunitacion.h
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,9 @@
- (void) writeDataToAgda:(NSString *) message sender:(NSViewController *)sender;
- (void) searchForAgda;
- (BOOL) isAgdaAvaliableAtPath:(NSString *)path;
- (void) openConnectionToAgda;
- (void) closeConnectionToAgda;
- (void) quitAndRestartConnectionToAgda;
- (void) clearPartialResponse;

- (void) openConnectionToAgda;

@end
23 changes: 19 additions & 4 deletions Agda Writer/AWCommunitacion.m
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#import "AWNotifications.h"
#import "AWAgdaParser.h"
#import "AWAgdaActions.h"
#import "AWHelper.h"

@implementation AWCommunitacion

Expand Down Expand Up @@ -196,12 +197,26 @@ - (void) openConnectionToAgda
[task setStandardOutput: [NSPipe pipe]];
[task setStandardInput: [NSPipe pipe]];
[task setStandardError: [task standardOutput]];
[task setEnvironment:@{@"Agda_datadir" : @"/Users/andrej/Documents/agda-writer/agda/Agda-2.4.0.2",
@"DYLD_FALLBACK_LIBRARY_PATH" : @"/Users/andrej/Documents/agda-writer/agda"}];
BOOL useBundledAgda = [[NSUserDefaults standardUserDefaults] boolForKey:@"useBundledAgda"];
if (useBundledAgda) {
NSDictionary * environmentDictionary = @{
@"Agda_datadir" : [AWHelper pathToBundledAgdaPrimitive],
@"DYLD_FALLBACK_LIBRARY_PATH" : [AWHelper pathToBundledAgda]
};
[task setLaunchPath:[AWHelper pathToBundledAgda]];
[task setEnvironment:environmentDictionary];
}
else {
[task setLaunchPath:[AWNotifications agdaLaunchPath]];
}
// [task setEnvironment:@{@"Agda_datadir" : @"/Users/andrej/Documents/agda-writer/agda/Agda-2.4.0.2",
// @"DYLD_FALLBACK_LIBRARY_PATH" : @"/Users/andrej/Documents/agda-writer/agda"}];


[task setLaunchPath:[AWNotifications agdaLaunchPath]];
// [task setLaunchPath:@"/Users/markokoleznik/Library/Haskell/bin/agda"];
[task setArguments:@[@"--interaction"]];

NSLog(@"Agda launch path:\n%@", task.launchPath);

[[[task standardOutput] fileHandleForReading] waitForDataInBackgroundAndNotify];

// Add observer
Expand Down
2 changes: 2 additions & 0 deletions Agda Writer/AWHelper.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,5 +24,7 @@

+ (NSString *) helpForExternalLibraries;

+ (NSString *) pathToBundledAgda;
+ (NSString *) pathToBundledAgdaPrimitive;

@end
8 changes: 8 additions & 0 deletions Agda Writer/AWHelper.m
Original file line number Diff line number Diff line change
Expand Up @@ -113,4 +113,12 @@ + (NSString *) helpForExternalLibraries {
return @"Explanation: Libraries, which you can import when loading a file, for example stdlib. If you want to use multiple libraries, separate them with comma (,)\n\nUsage: You should put full path, ~ stands for relative to current work path.\n\nExample: /Users/username/AgdaLibs";
}

+ (NSString *) pathToBundledAgda {
return [[NSBundle mainBundle] pathForResource:@"agda" ofType:@""];
}
+ (NSString *) pathToBundledAgdaPrimitive {
NSString * pathToAgdaDirectory = [NSString stringWithFormat:@"%@%@", [[NSBundle mainBundle] resourcePath], @"/Agda-2.4.2.2"];;
return pathToAgdaDirectory;
}

@end
12 changes: 11 additions & 1 deletion Agda Writer/AppDelegate.m
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,12 @@ @implementation AppDelegate

- (void)applicationDidFinishLaunching:(NSNotification *)aNotification {
// Insert code here to initialize your application

// check for agda!
if ([[AWNotifications agdaLaunchPath] isEqualToString:@""]) {
// agda path is not yet set


BOOL isPathToAgdaSet = NO;

NSArray * reasonablePlacesForAgda =
@[
Expand All @@ -35,9 +36,18 @@ - (void)applicationDidFinishLaunching:(NSNotification *)aNotification {

if ([self isAgdaAvaliableAtPath:path]) {
[AWNotifications setAgdaLaunchPath:path];
isPathToAgdaSet = YES;
[[NSUserDefaults standardUserDefaults] setObject:[NSNumber numberWithBool:NO] forKey:@"useBundledAgda"];
break;
}
}


if (!isPathToAgdaSet) {
// If everything fails, load agda from Agda Writer's folder.
// Don't forget to use custom dictionary with appropriate arguments (dictionary).
[[NSUserDefaults standardUserDefaults] setObject:[NSNumber numberWithBool:YES] forKey:@"useBundledAgda"];
}
}


Expand Down
17 changes: 16 additions & 1 deletion Agda Writer/Base.lproj/Main.storyboard
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<document type="com.apple.InterfaceBuilder3.Cocoa.Storyboard.XIB" version="3.0" toolsVersion="8191" systemVersion="15A284" targetRuntime="MacOSX.Cocoa" propertyAccessControl="none" useAutolayout="YES">
<dependencies>
<deployment identifier="macosx"/>
<plugIn identifier="com.apple.InterfaceBuilder.CocoaPlugin" version="8191"/>
</dependencies>
<scenes>
Expand Down Expand Up @@ -848,6 +847,11 @@
</textFieldCell>
<connections>
<action selector="pathSelected:" target="izb-Gj-tQA" id="LgX-XA-ukR"/>
<binding destination="xp5-Sa-wkr" name="enabled" keyPath="values.useBundledAgda" id="l0g-jr-wnq">
<dictionary key="options">
<string key="NSValueTransformerName">NSNegateBoolean</string>
</dictionary>
</binding>
<outlet property="delegate" destination="izb-Gj-tQA" id="vTx-24-fBP"/>
</connections>
</textField>
Expand Down Expand Up @@ -1015,6 +1019,17 @@
<action selector="showHelpForExternalLibraries:" target="izb-Gj-tQA" id="hZ2-iF-MuZ"/>
</connections>
</button>
<button fixedFrame="YES" translatesAutoresizingMaskIntoConstraints="NO" id="e53-nj-kuj">
<rect key="frame" x="329" y="310" width="134" height="18"/>
<animations/>
<buttonCell key="cell" type="check" title="Use Bundled Agda" bezelStyle="regularSquare" imagePosition="left" state="on" inset="2" id="trE-1v-AIb">
<behavior key="behavior" changeContents="YES" doesNotDimImage="YES" lightByContents="YES"/>
<font key="font" metaFont="system"/>
</buttonCell>
<connections>
<binding destination="xp5-Sa-wkr" name="value" keyPath="values.useBundledAgda" id="VGh-C6-O25"/>
</connections>
</button>
</subviews>
<constraints>
<constraint firstItem="uC9-3W-1j9" firstAttribute="leading" secondItem="nta-dI-OOZ" secondAttribute="leading" constant="137" id="01j-fH-38d"/>
Expand Down
33 changes: 33 additions & 0 deletions Agda Writer/agda/Agda-2.4.2.2/Agda.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
/* Aspects. */
.Comment { color: #B22222 }
.Keyword { color: #CD6600 }
.String { color: #B22222 }
.Number { color: #A020F0 }
.Symbol { color: #404040 }
.PrimitiveType { color: #0000CD }
.Operator {}

/* NameKinds. */
.Bound { color: black }
.InductiveConstructor { color: #008B00 }
.CoinductiveConstructor { color: #8B7500 }
.Datatype { color: #0000CD }
.Field { color: #EE1289 }
.Function { color: #0000CD }
.Module { color: #A020F0 }
.Postulate { color: #0000CD }
.Primitive { color: #0000CD }
.Record { color: #0000CD }

/* OtherAspects. */
.DottedPattern {}
.UnsolvedMeta { color: black; background: yellow }
.UnsolvedConstraint { color: black; background: yellow }
.TerminationProblem { color: black; background: #FFA07A }
.IncompletePattern { color: black; background: #F5DEB3 }
.Error { color: red; text-decoration: underline }
.TypeChecks { color: black; background: #ADD8E6 }

/* Standard attributes. */
a { text-decoration: none }
a[href]:hover { background-color: #B4EEB4 }
Loading

0 comments on commit d1b4e20

Please sign in to comment.