diff --git a/Cargo.lock b/Cargo.lock index 0a807f9..68cba59 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -25,7 +25,7 @@ checksum = "080e9890a082662b09c1ad45f567faeeb47f22b5fb23895fbe1e651e718e25ca" [[package]] name = "argus-cli" -version = "0.1.10" +version = "0.1.11" dependencies = [ "anyhow", "argus-ext", @@ -42,7 +42,7 @@ dependencies = [ [[package]] name = "argus-ext" -version = "0.1.10" +version = "0.1.11" dependencies = [ "anyhow", "fluid-let", @@ -55,7 +55,7 @@ dependencies = [ [[package]] name = "argus-lib" -version = "0.1.10" +version = "0.1.11" dependencies = [ "anyhow", "argus-ext", @@ -80,7 +80,7 @@ dependencies = [ [[package]] name = "argus-ser" -version = "0.1.10" +version = "0.1.11" dependencies = [ "anyhow", "argus-ext", diff --git a/crates/argus/src/analysis/entry.rs b/crates/argus/src/analysis/entry.rs index 61f8d6d..578d362 100644 --- a/crates/argus/src/analysis/entry.rs +++ b/crates/argus/src/analysis/entry.rs @@ -209,24 +209,8 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>( body_id: BodyId, typeck_results: &'tcx TypeckResults<'tcx>, ) -> (Forgettable>, ObligationsInBody) { - let mut obligations = tls::take_obligations(); - let obligation_data = tls::unsafe_take_data(); - let obligation_data = FullData::new(obligation_data); - - // XXX: it's possible that Argus reports false negatives. Meaning that - // in a body that type checks, failing obligations are reported. - // This happens as a result of how predicates are extracted from rustc (ask gavin) - // so as a first heuristic, if the body isn't tainted by errors, we'll just remove - // all non-successful obligations. - if typeck_results.tainted_by_errors.is_none() { - log::debug!( - "Removing failures: Body not-tainted {:?}", - typeck_results.hir_owner - ); - obligations.retain(|prov| prov.it.result.is_yes()); - } else { - log::debug!("Body tainted! {:?}", typeck_results.hir_owner); - } + let obligations = tls::take_obligations(); + let obligation_data = FullData::new(tls::unsafe_take_data()); let ctx = ErrorAssemblyCtx { tcx, diff --git a/crates/argus/src/analysis/transform.rs b/crates/argus/src/analysis/transform.rs index e471a3c..8ae9539 100644 --- a/crates/argus/src/analysis/transform.rs +++ b/crates/argus/src/analysis/transform.rs @@ -148,6 +148,7 @@ pub fn transform<'a, 'tcx: 'a>( ObligationsInBody::new( name, + typeck_results.tainted_by_errors.is_some(), body_range, builder.ambiguity_errors, builder.trait_errors, diff --git a/crates/argus/src/proof_tree/mod.rs b/crates/argus/src/proof_tree/mod.rs index 8f71fc6..c068454 100644 --- a/crates/argus/src/proof_tree/mod.rs +++ b/crates/argus/src/proof_tree/mod.rs @@ -13,6 +13,7 @@ use index_vec::IndexVec; use rustc_infer::infer::InferCtxt; use rustc_middle::ty; use serde::Serialize; +use serde_json as json; pub use topology::*; #[cfg(feature = "testing")] use ts_rs::TS; @@ -48,7 +49,7 @@ pub enum Node { #[cfg_attr(feature = "testing", ts(export))] pub struct GoalData { #[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))] - value: serde_json::Value, + value: json::Value, necessity: ObligationNecessity, num_vars: usize, @@ -69,7 +70,7 @@ pub struct GoalData { pub enum CandidateData { Impl { #[cfg_attr(feature = "testing", ts(type = "ImplHeader"))] - hd: serde_json::Value, + hd: json::Value, is_user_visible: bool, }, ParamEnv(usize), @@ -106,11 +107,11 @@ pub struct SerializedTree { pub results: IndexVec, #[cfg_attr(feature = "testing", ts(type = "TyVal[]"))] - pub tys: IndexVec, + pub tys: IndexVec, pub projection_values: HashMap, - pub all_impl_candidates: HashMap>, + pub all_impl_candidates: HashMap, pub topology: TreeTopology, @@ -120,6 +121,17 @@ pub struct SerializedTree { pub analysis: aadebug::AnalysisResults, } +#[derive(Serialize, Debug, Clone)] +#[serde(rename_all = "camelCase")] +#[cfg_attr(feature = "testing", derive(TS))] +#[cfg_attr(feature = "testing", ts(export))] +pub struct Implementors { + #[cfg_attr(feature = "testing", ts(type = "TraitRefPrintOnlyTraitPath"))] + pub _trait: json::Value, + + pub impls: Vec, +} + #[derive(Serialize, Debug, Clone)] #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export))] diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs index cd64234..f1784de 100644 --- a/crates/argus/src/proof_tree/serialize.rs +++ b/crates/argus/src/proof_tree/serialize.rs @@ -25,7 +25,7 @@ pub struct SerializedTreeVisitor<'tcx> { pub topology: TreeTopology, pub cycle: Option, pub projection_values: HashMap, - pub all_impl_candidates: HashMap>, + pub all_impl_candidates: HashMap, deferred_leafs: Vec<(ProofNodeIdx, EvaluationResult)>, interners: Interners, @@ -243,14 +243,26 @@ impl<'tcx> SerializedTreeVisitor<'tcx> { // If the Goal is a TraitPredicate we will cache *all* possible implementors if let Some(tp) = goal.goal().predicate.as_trait_predicate() { let infcx = goal.infcx(); + + // Make Trait ref name + // FIXME: this is a mega hack + let _trait = + ser::TraitRefPrintOnlyTraitPathDef(tp.skip_binder().trait_ref); + + let _trait = tls::unsafe_access_interner(|ty_interner| { + ser::to_value_expect(infcx, ty_interner, &_trait) + }); + + // Gather all impls + let mut impls = vec![]; for can in infcx.find_similar_impl_candidates(tp) { let can_idx = self.interners.intern_impl(infcx, can.impl_def_id); - self - .all_impl_candidates - .entry(idx) - .or_default() - .push(can_idx); + impls.push(can_idx); } + + self + .all_impl_candidates + .insert(idx, Implementors { _trait, impls }); } } } diff --git a/crates/argus/src/types.rs b/crates/argus/src/types.rs index d19e664..7acad8f 100644 --- a/crates/argus/src/types.rs +++ b/crates/argus/src/types.rs @@ -134,6 +134,8 @@ pub struct ObligationsInBody { /// Range of the represented body. pub range: CharRange, + pub is_tainted: bool, + /// All ambiguous expression in the body. These *could* involve /// trait errors, so it's important that we can map the specific /// obligations to these locations. (That is, if they occur.) @@ -157,6 +159,7 @@ pub struct ObligationsInBody { impl ObligationsInBody { pub fn new( id: Option<(&InferCtxt, DefId)>, + is_tainted: bool, range: CharRange, ambiguity_errors: IndexSet, trait_errors: Vec, @@ -174,6 +177,7 @@ impl ObligationsInBody { name: json_name, hash: BodyHash::new(), range, + is_tainted, ambiguity_errors, trait_errors, obligations, diff --git a/ide/packages/common/src/BodyInfo.ts b/ide/packages/common/src/BodyInfo.ts index 1d7cad1..411197d 100644 --- a/ide/packages/common/src/BodyInfo.ts +++ b/ide/packages/common/src/BodyInfo.ts @@ -8,7 +8,7 @@ import type { ObligationIdx, ObligationsInBody } from "./bindings"; -import { isVisibleObligation } from "./func"; +// import { isVisibleObligation } from "./func"; class BodyInfo { private existsImportantFailure; @@ -29,12 +29,20 @@ class BodyInfo { ); } + get isTainted(): boolean { + return this.oib.isTainted; + } + get hash(): BodyHash { return this.oib.hash; } get numErrors(): number { - return this.oib.ambiguityErrors.length + this.oib.traitErrors.length; + // NOTE: is the body isn't tainted by errors, the number of errors + // is ZERO, even if Argus sends errors to the frontend. + return !this.isTainted + ? 0 + : this.oib.ambiguityErrors.length + this.oib.traitErrors.length; } get name() { @@ -100,18 +108,25 @@ class BodyInfo { isVisible(idx: ObligationIdx) { const o = this.obligation(idx); if (o === undefined) return false; + // If the body isn't tainted by errors, we only show obligations that hold true. + if (!this.isTainted && o.result !== "yes") return false; - return ( - this.showHidden || - isVisibleObligation( - o, + const _isVisibleObligation = () => + // Short-circuit ambiguities if we're filtering them + !( + (o.result === "maybe-ambiguity" || o.result === "maybe-overflow") && // HACK: If there is a failing obligation, we filter ambiguities. This is // a short workaround for a backend incompleteness. We can't filter obligations // that get resolved in a second round of trait solving, this leaves Argus with // more "failures" than rustc shows. this.existsImportantFailure - ) - ); + ) && + // If the obligation is listed as necessary, it's visible + (o.necessity === "Yes" || + // If the obligation is listed as necessary on error, and it failed, it's visible + (o.necessity === "OnError" && o.result === "no")); + + return this.showHidden || _isVisibleObligation(); } } diff --git a/ide/packages/common/src/TreeInfo.ts b/ide/packages/common/src/TreeInfo.ts index 048c73d..65da1d9 100644 --- a/ide/packages/common/src/TreeInfo.ts +++ b/ide/packages/common/src/TreeInfo.ts @@ -6,6 +6,7 @@ import type { EvaluationResult, GoalIdx, GoalKind, + Implementors, ProofNodeIdx, ResultIdx, SerializedTree, @@ -442,7 +443,7 @@ export class TreeInfo { return _.min(_.map(hs, TreeInfo.setInertia)) ?? 10_000; } - public implCandidates(idx: ProofNodeIdx): CandidateIdx[] | undefined { + public implCandidates(idx: ProofNodeIdx): Implementors | undefined { return this.tree.allImplCandidates[idx]; } } diff --git a/ide/packages/common/src/context.ts b/ide/packages/common/src/context.ts index 913380d..7840a22 100644 --- a/ide/packages/common/src/context.ts +++ b/ide/packages/common/src/context.ts @@ -10,13 +10,19 @@ import type { SystemSpec } from "./lib"; +export const settingsToggles = ["show-hidden-obligations"] as const; + +export type Settings = { + [K in (typeof settingsToggles)[number]]: boolean; +}; + export const AppContext = { MessageSystemContext: createContext(undefined), ConfigurationContext: createContext< (PanoptesConfig & { evalMode: EvaluationMode }) | undefined >(undefined), SystemSpecContext: createContext(undefined), - ShowHiddenObligationsContext: createContext(false) + SettingsContext: createContext({ "show-hidden-obligations": false }) }; export const FileContext = createContext(undefined); diff --git a/ide/packages/common/src/func.ts b/ide/packages/common/src/func.ts index 98ab8c7..d8ead52 100644 --- a/ide/packages/common/src/func.ts +++ b/ide/packages/common/src/func.ts @@ -5,10 +5,8 @@ import type { BoundTyKind, BoundVariableKind, CharRange, - EvaluationResult, GenericArg, ObligationHash, - ObligationNecessity, Predicate, Region, Ty, @@ -67,19 +65,10 @@ export function makeHighlightPosters( return [addHighlight, removeHighlight]; } -export const isVisibleObligation = ( - o: { necessity: ObligationNecessity; result: EvaluationResult }, - filterAmbiguities = false -) => - // Short-circuit ambiguities if we're filtering them - !( - (o.result === "maybe-ambiguity" || o.result === "maybe-overflow") && - filterAmbiguities - ) && - // If the obligation is listed as necessary, it's visible - (o.necessity === "Yes" || - // If the obligation is listed as necessary on error, and it failed, it's visible - (o.necessity === "OnError" && o.result === "no")); +export const composeEvents = + (...es: (((t: T) => void) | undefined)[]) => + (t: T) => + _.forEach(es, e => (e ? e(t) : {})); export function searchObject(obj: any, target: any) { for (let key in obj) { diff --git a/ide/packages/panoptes/src/App.css b/ide/packages/panoptes/src/App.css index bff7a5d..4907a76 100644 --- a/ide/packages/panoptes/src/App.css +++ b/ide/packages/panoptes/src/App.css @@ -1,5 +1,5 @@ #root { - font-size: var(--vscode-editor-font-size); + font-size: var(--vscode-font-size); } .app-nav { @@ -20,6 +20,22 @@ margin-bottom: 0.25em; } +.SettingsArea { + display: flex; + flex-direction: column; + gap: 0.5em; + justify-content: flex-start; +} + +.SettingsIco { + padding: 0.25em; +} + +.SettingsIco > i:hover { + cursor: pointer; + color: var(--vscode-input-placeholderForeground); +} + .DefinitionWrapper.hovered.meta-pressed { color: var(--vscode-editorLink-activeForeground); text-decoration: underline; diff --git a/ide/packages/panoptes/src/App.tsx b/ide/packages/panoptes/src/App.tsx index 07a3188..b51c1e9 100644 --- a/ide/packages/panoptes/src/App.tsx +++ b/ide/packages/panoptes/src/App.tsx @@ -3,7 +3,11 @@ import { createClosedMessageSystem, vscodeMessageSystem } from "@argus/common/communication"; -import { AppContext } from "@argus/common/context"; +import { + AppContext, + type Settings, + settingsToggles +} from "@argus/common/context"; import { type EvaluationMode, type FileInfo, @@ -15,7 +19,7 @@ import { isSysMsgPin, isSysMsgUnpin } from "@argus/common/lib"; -import { IcoComment } from "@argus/print/Icons"; +import { IcoComment, IcoSettingsGear } from "@argus/print/Icons"; import { DefPathRender, LocationActionable, @@ -36,6 +40,7 @@ import type { } from "@argus/print/context"; import { PrintTyValue } from "@argus/print/lib"; import classNames from "classnames"; +import Floating from "./Floating"; import MiniBuffer from "./MiniBuffer"; import Workspace from "./Workspace"; import { HighlightTargetStore, MiniBufferDataStore } from "./signals"; @@ -216,9 +221,21 @@ const CustomProjectionRender = observer( } ); +const SettingsPortal = ({ children }: React.PropsWithChildren) => ( + }> + {children} + +); + +const settingsKeyText = (key: keyof Settings) => _.upperFirst(_.lowerCase(key)); + const App = observer(({ config }: { config: PanoptesConfig }) => { const [openFiles, setOpenFiles] = useState(buildInitialData(config)); - const [showHidden, setShowHidden] = useState(false); + const [settings, setSettings] = useState({ + "show-hidden-obligations": false + }); + const toggleSetting = (key: keyof Settings) => + setSettings(curr => ({ ...curr, [key]: !curr[key] })); const messageSystem = config.type === "WEB_BUNDLE" @@ -253,12 +270,19 @@ const App = observer(({ config }: { config: PanoptesConfig }) => { const Navbar = ( <>
- setShowHidden(!showHidden)} - checked={showHidden} - > - Show hidden information - + +
+ {_.map(settingsToggles, (key, idx) => ( + toggleSetting(key)} + checked={settings[key]} + > + {settingsKeyText(key)} + + ))} +
+
@@ -270,7 +294,7 @@ const App = observer(({ config }: { config: PanoptesConfig }) => { - + { - + diff --git a/ide/packages/panoptes/src/Expr.tsx b/ide/packages/panoptes/src/Expr.tsx index 850f4e2..9c47d37 100644 --- a/ide/packages/panoptes/src/Expr.tsx +++ b/ide/packages/panoptes/src/Expr.tsx @@ -26,14 +26,10 @@ const Expr = observer(({ idx }: { idx: ExprIdx }) => { file ); - if (expr.isBody && !bodyInfo.showHidden) { - return null; - } + if (expr.isBody && !bodyInfo.showHidden) return null; const visibleObligations = bodyInfo.obligations(idx); - if (visibleObligations.length === 0) { - return null; - } + if (visibleObligations.length === 0) return null; const Content = () => _.map(visibleObligations, (oi, i) => ( diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx index c7b5b5a..660f05f 100644 --- a/ide/packages/panoptes/src/File.tsx +++ b/ide/packages/panoptes/src/File.tsx @@ -6,12 +6,13 @@ import { FileContext } from "@argus/common/context"; import type { Filename } from "@argus/common/lib"; -import ErrorDiv from "@argus/print/ErrorDiv"; +import { ErrorDiv, InfoDiv } from "@argus/print/Info"; import MonoSpace from "@argus/print/MonoSpace"; import ReportBugUrl from "@argus/print/ReportBugUrl"; import { TyCtxt } from "@argus/print/context"; import { PrintBodyName } from "@argus/print/lib"; -import { VSCodeDivider } from "@vscode/webview-ui-toolkit/react"; +import { nbsp } from "@argus/print/syntax"; +import { VSCodeBadge, VSCodeDivider } from "@vscode/webview-ui-toolkit/react"; import _ from "lodash"; import { observer } from "mobx-react"; import React, { Fragment, useContext } from "react"; @@ -37,7 +38,10 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => { const errCount = bodyInfo.numErrors > 0 ? ( - ({bodyInfo.numErrors}) + <> + {nbsp} + {bodyInfo.numErrors} + ) : null; const header = ( @@ -73,8 +77,11 @@ export interface FileProps { } const File = ({ file, osibs }: FileProps) => { - const showHidden = useContext(AppContext.ShowHiddenObligationsContext); - const bodyInfos = _.map(osibs, osib => new BodyInfo(osib, showHidden)); + const settings = useContext(AppContext.SettingsContext); + const bodyInfos = _.map( + osibs, + osib => new BodyInfo(osib, settings["show-hidden-obligations"]) + ); const noBodiesFound = ( @@ -89,12 +96,30 @@ const File = ({ file, osibs }: FileProps) => { ); + const fileTypecks = ( + +

+ Argus thinks this file type checks! You may close the Argus inspector + panel. If you think it shouldn’t, please click below to report this as a + bug! +

+ +
+ ); + const bodiesWithVisibleExprs = _.filter(bodyInfos, bi => bi.hasVisibleExprs() ); if (bodiesWithVisibleExprs.length === 0) { - return noBodiesFound; + if (_.some(bodyInfos, bi => bi.isTainted)) { + return noBodiesFound; + } else { + return fileTypecks; + } } return ( diff --git a/ide/packages/panoptes/src/Floating.css b/ide/packages/panoptes/src/Floating.css new file mode 100644 index 0000000..1e2f240 --- /dev/null +++ b/ide/packages/panoptes/src/Floating.css @@ -0,0 +1,11 @@ +.floating { + background-color: var(--vscode-dropdown-background); + color: var(--vscode-dropdown-foreground); + border: 1.5px solid var(--vscode-dropdown-border); + border-radius: 3px; + padding: 0.25em; +} + +svg.floating-arrow { + fill: var(--vscode-dropdown-border); +} \ No newline at end of file diff --git a/ide/packages/panoptes/src/Floating.tsx b/ide/packages/panoptes/src/Floating.tsx new file mode 100644 index 0000000..741002b --- /dev/null +++ b/ide/packages/panoptes/src/Floating.tsx @@ -0,0 +1,97 @@ +import React, { useRef, useState } from "react"; + +import { composeEvents } from "@argus/common/func"; +import { + FloatingArrow, + FloatingFocusManager, + FloatingPortal, + arrow, + autoUpdate, + flip, + offset, + shift, + useClick, + useDismiss, + useFloating, + useInteractions +} from "@floating-ui/react"; +import classNames from "classnames"; + +import "./Floating.css"; + +export interface FloatingProps { + toggle: React.JSX.Element; + outerClassName?: string; + innerClassName?: string; + reportActive?: (b: boolean) => void; +} + +const Floating = (props: React.PropsWithChildren) => { + const [isOpen, setIsOpen] = useState(false); + const openCallback = composeEvents(setIsOpen, props.reportActive); + const arrowRef = useRef(null); + + const ARROW_HEIGHT = 10; + const GAP = 5; + + const { refs, floatingStyles, context } = useFloating({ + open: isOpen, + onOpenChange: openCallback, + placement: "bottom", + middleware: [ + offset(ARROW_HEIGHT + GAP), + flip(), + shift(), + arrow({ + element: arrowRef + }) + ], + whileElementsMounted: autoUpdate + }); + + const click = useClick(context); + const dismiss = useDismiss(context); + const { getReferenceProps, getFloatingProps } = useInteractions([ + click, + dismiss + ]); + + return ( + <> + + {props.toggle} + + {isOpen && ( + + +
e.stopPropagation()} + > + + + + {props.children} +
+
+
+ )} + + ); +}; + +export default Floating; diff --git a/ide/packages/panoptes/src/Obligation.tsx b/ide/packages/panoptes/src/Obligation.tsx index a15f7da..73fd907 100644 --- a/ide/packages/panoptes/src/Obligation.tsx +++ b/ide/packages/panoptes/src/Obligation.tsx @@ -7,7 +7,7 @@ import type { import { BodyInfoContext, FileContext } from "@argus/common/context"; import { AppContext } from "@argus/common/context"; import { makeHighlightPosters, obligationCardId } from "@argus/common/func"; -import ErrorDiv from "@argus/print/ErrorDiv"; +import { ErrorDiv } from "@argus/print/Info"; import ReportBugUrl from "@argus/print/ReportBugUrl"; import { PrintObligation } from "@argus/print/lib"; import { observer } from "mobx-react"; diff --git a/ide/packages/panoptes/src/TreeView/Erotisi.tsx b/ide/packages/panoptes/src/TreeView/Erotisi.tsx index b6bc699..312b384 100644 --- a/ide/packages/panoptes/src/TreeView/Erotisi.tsx +++ b/ide/packages/panoptes/src/TreeView/Erotisi.tsx @@ -1,8 +1,8 @@ import type { TreeInfo } from "@argus/common/TreeInfo"; import type { ProofNodeIdx, SetHeuristic } from "@argus/common/bindings"; import { TreeAppContext } from "@argus/common/context"; -import ErrorDiv from "@argus/print/ErrorDiv"; import Indented from "@argus/print/Indented"; +import { ErrorDiv } from "@argus/print/Info"; import ReportBugUrl from "@argus/print/ReportBugUrl"; import { VSCodeButton } from "@vscode/webview-ui-toolkit/react"; import _ from "lodash"; diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.css b/ide/packages/panoptes/src/TreeView/Wrappers.css index bffb6f7..552f03e 100644 --- a/ide/packages/panoptes/src/TreeView/Wrappers.css +++ b/ide/packages/panoptes/src/TreeView/Wrappers.css @@ -8,19 +8,18 @@ } .floating-graph { - box-shadow: 0 0 5px 0 var(--vscode-focusBorder); max-height: 70vh; - overflow-y: auto; - overflow-x: hidden; - width: 90%; + max-width: 80%; + overflow: scroll; + box-shadow: 0 0 5px 0 var(--vscode-focusBorder); } .ImplCandidatesPanel { - padding: 0.5em; -} - -.ImplCandidatesPanel > div { - margin-bottom: 1em; + padding: 1em; + gap: 1.5em; + display: flex; + flex-direction: column; + justify-content: flex-start; } .WrapperBox { diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.tsx b/ide/packages/panoptes/src/TreeView/Wrappers.tsx index 9c25041..0ce2850 100644 --- a/ide/packages/panoptes/src/TreeView/Wrappers.tsx +++ b/ide/packages/panoptes/src/TreeView/Wrappers.tsx @@ -6,25 +6,16 @@ import type { import { TreeAppContext } from "@argus/common/context"; import { arrUpdate } from "@argus/common/func"; import { IcoListUL, IcoTreeDown } from "@argus/print/Icons"; -import { - FloatingArrow, - FloatingFocusManager, - FloatingPortal, - arrow, - offset, - shift, - useClick, - useDismiss, - useFloating, - useInteractions -} from "@floating-ui/react"; +import {} from "@floating-ui/react"; import classNames from "classnames"; import _ from "lodash"; -import React, { type ReactElement, useState, useContext, useRef } from "react"; +import React, { type ReactElement, useState, useContext } from "react"; import Graph from "./Graph"; import { Candidate } from "./Node"; import "./Wrappers.css"; +import { PrintDefPath } from "@argus/print/lib"; +import Floating from "../Floating"; export const WrapNode = ({ children, @@ -58,79 +49,22 @@ export const WrapNode = ({ ); }; -const composeEvents = - (...es: ((t: T) => void)[]) => - (t: T) => - _.forEach(es, e => e(t)); - const DetailsPortal = ({ children, info, reportActive }: React.PropsWithChildren< Omit & { info: ReactElement } ->) => { - const [isOpen, setIsOpen] = useState(false); - const openCallback = composeEvents(setIsOpen, reportActive); - const arrowRef = useRef(null); - - const ARROW_HEIGHT = 10; - const GAP = 5; - - const { refs, floatingStyles, context } = useFloating({ - open: isOpen, - onOpenChange: openCallback, - placement: "bottom", - middleware: [ - offset(ARROW_HEIGHT + GAP), - shift(), - arrow({ - element: arrowRef - }) - ] - }); - - const click = useClick(context); - const dismiss = useDismiss(context); - const { getReferenceProps, getFloatingProps } = useInteractions([ - click, - dismiss - ]); - - return ( - <> - - {info} - - {isOpen && ( - - -
e.stopPropagation()} - > - - {children} -
-
-
- )} - - ); -}; +>) => ( + + {children} + +); export const WrapTreeIco = ({ n, reportActive }: InfoWrapperProps) => ( }> @@ -140,14 +74,18 @@ export const WrapTreeIco = ({ n, reportActive }: InfoWrapperProps) => ( export const WrapImplCandidates = ({ n, reportActive }: InfoWrapperProps) => { const tree = useContext(TreeAppContext.TreeContext)!; - const candidates = tree.implCandidates(n); - if (candidates === undefined || candidates.length === 0) return null; + const implementors = tree.implCandidates(n); + if (implementors === undefined || implementors.impls.length === 0) + return null; return ( }> -

The following {candidates.length} implementations are available:

+

+ There are {implementors.impls.length}{" "} + implementors +

- {_.map(candidates, (c, i) => ( + {_.map(implementors.impls, (c, i) => (
diff --git a/ide/packages/print/src/ErrorDiv.css b/ide/packages/print/src/ErrorDiv.css deleted file mode 100644 index 4994286..0000000 --- a/ide/packages/print/src/ErrorDiv.css +++ /dev/null @@ -1,7 +0,0 @@ -.ErrorDiv { - padding: 0.5em; - border-radius: 3px; - border-width: 2px; - border-color: var(--vscode-inputValidation-errorBorder); - background: var(--vscode-inputValidation-errorBackground) -} \ No newline at end of file diff --git a/ide/packages/print/src/ErrorDiv.tsx b/ide/packages/print/src/ErrorDiv.tsx deleted file mode 100644 index b76efb3..0000000 --- a/ide/packages/print/src/ErrorDiv.tsx +++ /dev/null @@ -1,9 +0,0 @@ -import React from "react"; - -import "./ErrorDiv.css"; - -const ErrorDiv = ({ children }: React.PropsWithChildren<{}>) => ( -
{children}
-); - -export default ErrorDiv; diff --git a/ide/packages/print/src/HoverInfo.css b/ide/packages/print/src/HoverInfo.css index 7da8308..51092a4 100644 --- a/ide/packages/print/src/HoverInfo.css +++ b/ide/packages/print/src/HoverInfo.css @@ -1,11 +1,3 @@ .HoverMainInfo { display: inline; } - -.floating { - background-color: var(--vscode-dropdown-background); - color: var(--vscode-dropdown-foreground); - border: 1.5px solid var(--vscode-dropdown-border); - border-radius: 3px; - padding: 0.25em; - } \ No newline at end of file diff --git a/ide/packages/print/src/Icons.tsx b/ide/packages/print/src/Icons.tsx index 87fefbc..58ace0a 100644 --- a/ide/packages/print/src/Icons.tsx +++ b/ide/packages/print/src/Icons.tsx @@ -7,7 +7,7 @@ type ButtonProps = { onClick?: (event: React.MouseEvent) => void; }; -const makeCodicon = +const codicon = (name: string) => (props: React.HTMLAttributes & ButtonProps) => ( ( +
{children}
+); + +export const InfoDiv = ({ children }: React.PropsWithChildren) => ( +
{children}
+); diff --git a/ide/packages/print/src/MonoSpace.css b/ide/packages/print/src/MonoSpace.css index 2337a93..a509303 100644 --- a/ide/packages/print/src/MonoSpace.css +++ b/ide/packages/print/src/MonoSpace.css @@ -1,4 +1,4 @@ -.MonospaceArea { +.MonoSpaceArea { font-family: var(--vscode-editor-font-family); font-size: var(--vscode-editor-font-size); } \ No newline at end of file diff --git a/ide/packages/print/src/MonoSpace.tsx b/ide/packages/print/src/MonoSpace.tsx index 7170971..498d33c 100644 --- a/ide/packages/print/src/MonoSpace.tsx +++ b/ide/packages/print/src/MonoSpace.tsx @@ -1,12 +1,9 @@ import React, { type PropsWithChildren } from "react"; +import "./MonoSpace.css"; + const MonoSpace = ({ children }: PropsWithChildren) => ( - + {children} ); diff --git a/ide/packages/print/src/ReportBugUrl.tsx b/ide/packages/print/src/ReportBugUrl.tsx index bc77818..ad4da7a 100644 --- a/ide/packages/print/src/ReportBugUrl.tsx +++ b/ide/packages/print/src/ReportBugUrl.tsx @@ -1,6 +1,9 @@ import { AppContext } from "@argus/common/context"; import { getArgusIssueUrl } from "@argus/common/lib"; -import { VSCodeProgressRing } from "@vscode/webview-ui-toolkit/react"; +import { + VSCodeLink, + VSCodeProgressRing +} from "@vscode/webview-ui-toolkit/react"; import React, { useContext, useEffect, useState } from "react"; const PASTE_SUCCESS: number = 201; @@ -42,14 +45,14 @@ const ReportBugUrl = ({ }, []); return logState ? ( - {displayText} - + ) : ( <> building link ... diff --git a/ide/packages/print/src/lib.tsx b/ide/packages/print/src/lib.tsx index f349d30..a4bf90d 100644 --- a/ide/packages/print/src/lib.tsx +++ b/ide/packages/print/src/lib.tsx @@ -10,7 +10,7 @@ import type { import React from "react"; import { ErrorBoundary } from "react-error-boundary"; -import ErrorDiv from "./ErrorDiv"; +import { ErrorDiv } from "./Info"; import MonoSpace from "./MonoSpace"; import ReportBugUrl from "./ReportBugUrl"; import "./lib.css"; diff --git a/ide/packages/print/src/private/argus.tsx b/ide/packages/print/src/private/argus.tsx index db43c27..53f2f34 100644 --- a/ide/packages/print/src/private/argus.tsx +++ b/ide/packages/print/src/private/argus.tsx @@ -18,9 +18,9 @@ import React, { import classNames from "classnames"; import { Toggle } from "../Toggle"; import { AllowProjectionSubst, LocationActionable, TyCtxt } from "../context"; +import { Angled, CommaSeparated, Kw, PlusSeparated, nbsp } from "../syntax"; import { PrintDefinitionPath } from "./path"; import { PrintClause } from "./predicate"; -import { Angled, CommaSeparated, Kw, PlusSeparated, nbsp } from "./syntax"; import { PrintBinder, PrintGenericArg, diff --git a/ide/packages/print/src/private/const.tsx b/ide/packages/print/src/private/const.tsx index 079e2b5..d606ae1 100644 --- a/ide/packages/print/src/private/const.tsx +++ b/ide/packages/print/src/private/const.tsx @@ -7,8 +7,8 @@ import type { } from "@argus/common/bindings"; import React from "react"; +import { DBraced, Placeholder } from "../syntax"; import { PrintDefinitionPath, PrintValuePath } from "./path"; -import { DBraced, Placeholder } from "./syntax"; import { PrintExpr, PrintValueTree } from "./term"; import { PrintBoundVariable, PrintSymbol } from "./ty"; diff --git a/ide/packages/print/src/private/path.tsx b/ide/packages/print/src/private/path.tsx index 80fc31e..b8a2cd3 100644 --- a/ide/packages/print/src/private/path.tsx +++ b/ide/packages/print/src/private/path.tsx @@ -10,7 +10,7 @@ import { LocationActionable, TyCtxt } from "../context"; -import { Angled, CommaSeparated, Kw, nbsp } from "./syntax"; +import { Angled, CommaSeparated, Kw, nbsp } from "../syntax"; import { PrintGenericArg, PrintTy } from "./ty"; // A `DefinedPath` includes extra information about the definition location. diff --git a/ide/packages/print/src/private/predicate.tsx b/ide/packages/print/src/private/predicate.tsx index 2e3b8ca..6fb8e28 100644 --- a/ide/packages/print/src/private/predicate.tsx +++ b/ide/packages/print/src/private/predicate.tsx @@ -36,9 +36,12 @@ export const PrintPredicateObligation = ({ o }: { o: PredicateObligation }) => { ) ? null : ( ( - - - + <> +

Facts in the type environment

+ + + + )} > {" "} diff --git a/ide/packages/print/src/private/term.tsx b/ide/packages/print/src/private/term.tsx index 4a31068..a8028b3 100644 --- a/ide/packages/print/src/private/term.tsx +++ b/ide/packages/print/src/private/term.tsx @@ -11,16 +11,16 @@ import type { import _ from "lodash"; import React from "react"; -import { PrintConst } from "./const"; -import { PrintConstScalarInt } from "./const"; -import { PrintValuePath } from "./path"; import { Angled, CommaSeparated, DBraced, Parenthesized, SqBraced -} from "./syntax"; +} from "../syntax"; +import { PrintConst } from "./const"; +import { PrintConstScalarInt } from "./const"; +import { PrintValuePath } from "./path"; import { PrintSymbol, PrintTy } from "./ty"; export const PrintTerm = ({ o }: { o: Term }) => { diff --git a/ide/packages/print/src/private/ty.tsx b/ide/packages/print/src/private/ty.tsx index f88602c..9148449 100644 --- a/ide/packages/print/src/private/ty.tsx +++ b/ide/packages/print/src/private/ty.tsx @@ -48,8 +48,6 @@ import _, { isObject } from "lodash"; import React, { useContext } from "react"; import { Toggle } from "../Toggle"; import { AllowProjectionSubst, ProjectionPathRender, TyCtxt } from "../context"; -import { PrintConst } from "./const"; -import { PrintDefinitionPath } from "./path"; import { Angled, CommaSeparated, @@ -59,7 +57,9 @@ import { PlusSeparated, SqBraced, nbsp -} from "./syntax"; +} from "../syntax"; +import { PrintConst } from "./const"; +import { PrintDefinitionPath } from "./path"; import { PrintTerm } from "./term"; interface Binding { diff --git a/ide/packages/print/src/private/syntax.css b/ide/packages/print/src/syntax.css similarity index 100% rename from ide/packages/print/src/private/syntax.css rename to ide/packages/print/src/syntax.css diff --git a/ide/packages/print/src/private/syntax.tsx b/ide/packages/print/src/syntax.tsx similarity index 100% rename from ide/packages/print/src/private/syntax.tsx rename to ide/packages/print/src/syntax.tsx