Skip to content

Commit

Permalink
Widgets for Date_Time, Time_Of_Day and Time_Zone.
Browse files Browse the repository at this point in the history
  • Loading branch information
jdunkerley committed Jul 9, 2024
1 parent 71a6e21 commit 28536fe
Show file tree
Hide file tree
Showing 6 changed files with 59 additions and 6 deletions.
18 changes: 15 additions & 3 deletions app/gui2/src/util/net/dataServer.ts
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ export class DataServer extends ObservableV2<DataServerEvents> {
initialized: Promise<Result<void, Error>>
private initializationScheduled = false
resolveCallbacks = new Map<string, (data: any) => void>()
private hasConnected = false
private hasReceived = false

/** `websocket.binaryType` should be `ArrayBuffer`. */
constructor(
Expand All @@ -67,6 +69,7 @@ export class DataServer extends ObservableV2<DataServerEvents> {
abort.handleDispose(this)

websocket.addEventListener('message', ({ data: rawPayload }) => {
this.hasReceived = true
if (!(rawPayload instanceof ArrayBuffer)) {
console.warn('Data Server: Data type was invalid:', rawPayload)
// Ignore all non-binary messages. If the messages are `Blob`s instead, this is a
Expand All @@ -91,10 +94,15 @@ export class DataServer extends ObservableV2<DataServerEvents> {
this.emit(`${payloadType}`, [payload, uuid])
}
})
websocket.addEventListener('error', (error) =>
console.error('Language Server Binary socket error:', error),
)
websocket.addEventListener('error', (error) => {
console.error('Language Server Binary socket error:', error)
if (!this.hasReceived) {
console.error('Failed before receiving anything from the server')
this.websocket.close()
}
})
websocket.addEventListener('close', () => {
console.error('Websocket Closed.', this.hasConnected, this.hasReceived)
this.scheduleInitializationAfterConnect()
})

Expand All @@ -111,6 +119,9 @@ export class DataServer extends ObservableV2<DataServerEvents> {
this.initializationScheduled = true
this.initialized = new Promise((resolve) => {
const cb = () => {
console.error('Websocket Opened')
this.hasConnected = true
this.hasReceived = false
this.websocket.removeEventListener('open', cb)
this.initializationScheduled = false
resolve(this.initialize())
Expand All @@ -133,6 +144,7 @@ export class DataServer extends ObservableV2<DataServerEvents> {
result.error.log('Error initializing Language Server Binary Protocol')
return result
} else {
this.hasConnected = true
return Ok()
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -460,7 +460,7 @@ type Locale
to_display_text self = "Locale(" + self.to_text + ")"

## PRIVATE
Gets the default drop down option for this encoding.
Gets the default drop down option for Locale.
default_widget : Widget
default_widget = Widget.Single_Choice values=Locale.widget_options display=Display.When_Modified

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@ import project.Nothing.Nothing
import project.Panic.Panic
import project.Warning.Warning
from project.Data.Boolean import Boolean, False, True
from project.Data.Time.Date import make_day_picker
from project.Data.Text.Extensions import all
from project.Metadata import Display, Widget
from project.Widget_Helpers import make_date_time_format_selector

polyglot java import java.lang.ArithmeticException
Expand Down Expand Up @@ -148,6 +150,16 @@ type Date_Time
from Standard.Base import Date_Time, Time_Zone

example_new = Date_Time.new 1986 8 5
@year (Widget.Numeric_Input display=Display.Always)
@month (Widget.Numeric_Input minimum=1 maximum=12 display=Display.Always)
@day make_day_picker
@hour (Widget.Numeric_Input minimum=0 maximum=23 display=Display.Always)
@minute (Widget.Numeric_Input minimum=0 maximum=59 display=Display.Always)
@second (Widget.Numeric_Input minimum=0 maximum=59 display=Display.When_Modified)
@millisecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
@microsecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
@nanosecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
@zone Time_Zone.default_widget
new : Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Time_Zone -> Date_Time ! Time_Error
new year (month = 1) (day = 1) (hour = 0) (minute = 0) (second = 0) (millisecond = 0) (microsecond = 0) (nanosecond = 0) (zone = Time_Zone.system) =
total_nanoseconds = nanosecond + microsecond * 1000 + millisecond * 1000000
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import project.Nothing.Nothing
import project.Panic.Panic
from project.Data.Boolean import Boolean, False, True
from project.Data.Text.Extensions import all
from project.Metadata import Display, Widget
from project.Widget_Helpers import make_time_format_selector

polyglot java import java.lang.Exception as JException
Expand Down Expand Up @@ -92,6 +93,12 @@ type Time_Of_Day
from Standard.Base import Time_Of_Day

example_epoch = Time_Of_Day.new hour=9 minute=30
@hour (Widget.Numeric_Input minimum=0 maximum=23 display=Display.Always)
@minute (Widget.Numeric_Input minimum=0 maximum=59 display=Display.Always)
@second (Widget.Numeric_Input minimum=0 maximum=59 display=Display.When_Modified)
@millisecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
@microsecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
@nanosecond (Widget.Numeric_Input minimum=0 maximum=999 display=Display.When_Modified)
new : Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Time_Of_Day ! Time_Error
new (hour = 0) (minute = 0) (second = 0) (millisecond = 0) (microsecond = 0) (nanosecond = 0) =
total_nanoseconds = nanosecond + microsecond * 1000 + millisecond * 1000000
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,14 @@ import project.Data.Json.JS_Object
import project.Data.Numbers.Integer
import project.Data.Text.Text
import project.Data.Time.Date_Time.Date_Time
import project.Data.Vector.Vector
import project.Error.Error
import project.Errors.Illegal_Argument.Illegal_Argument
import project.Errors.Time_Error.Time_Error
import project.Panic.Panic
from project.Data.Boolean import Boolean, False, True
from project.Metadata import Display, make_single_choice, Widget
from project.Metadata.Choice import Option

polyglot java import java.lang.Exception as JException
polyglot java import java.time.ZoneId
Expand Down Expand Up @@ -107,8 +110,11 @@ type Time_Zone
from Standard.Base.Time.Time_Zone import Time_Zone

example_new = Time_Zone.new 1 1 50
@hours (Widget.Numeric_Input minimum=-18 maximum=18 display=Display.Always)
@minutes (Widget.Numeric_Input minimum=-59 maximum=59 display=Display.When_Modified)
@seconds (Widget.Numeric_Input minimum=-59 maximum=59 display=Display.When_Modified)
new : Integer -> Integer -> Integer -> Time_Zone
new (hours = 0) (minutes = 0) (seconds = 0) =
new (hours:Integer = 0) (minutes:Integer = 0) (seconds:Integer = 0) =
new_builtin hours minutes seconds

## ALIAS time zone from text
Expand Down Expand Up @@ -147,8 +153,9 @@ type Time_Zone
from Standard.Base import Time_Zone

example_parse = Time_Zone.parse "+03:02:01"
@id (make_single_choice Time_Zone.zone_names Display.Always)
parse : Text -> Time_Zone ! Time_Error
parse id =
parse id:Text =
Panic.catch JException handler=(catch -> Error.throw (Time_Error.Error catch.payload.getMessage)) <|
parse_builtin id

Expand Down Expand Up @@ -194,6 +201,17 @@ type Time_Zone
to_display_text : Text
to_display_text self = self.to_text

## PRIVATE
Gets the default drop down option for Time_Zone.
default_widget : Widget
default_widget =
options = [Option "System" "Time_Zone.system", Option "Local" "Time_Zone.local", Option "UTC" "Time_Zone.utc", Option "Named" "(Time_Zone.parse 'UTC')", Option "custom" "(Time_Zone.new 1 0 0)"]
Widget.Single_Choice values=options display=Display.When_Modified

## Gets a list of all the time zone names that are predefined.
zone_names : Vector Text
zone_names = Time_Utils.getZoneNames

## PRIVATE
Time_Zone.from (that:JS_Object) =
if that.get "type" == "Time_Zone" && ["id"].all that.contains_key then Time_Zone.parse (that.get "id") else
Expand Down
4 changes: 4 additions & 0 deletions std-bits/base/src/main/java/org/enso/base/Time_Utils.java
Original file line number Diff line number Diff line change
Expand Up @@ -246,4 +246,8 @@ public static void appendTwoDigitYear(
LocalDate baseDate = LocalDate.of(minYear, 1, 1);
builder.appendValueReduced(yearField, 2, 2, baseDate);
}

public static String[] getZoneNames() {
return ZoneId.getAvailableZoneIds().stream().toArray(String[]::new);
}
}

0 comments on commit 28536fe

Please sign in to comment.